/* Margins for the main body division */
div.main
	{ margin-left: 1%;
	margin-right: 1% }


/* Code fragments (structures, examples, etc.) */
pre
	{ color: #000000;
	font-family: Courier, monospace, serif }

/* Code references embedded in narrative */
code
	{ color: #800000;
	font-family: Courier, monospace, serif }

/* Code references embedded in narrative */
code.codeblue
	{ color: #0000FF;
	font-family: Courier, monospace, serif }


/* Code font (mainly for use in <A> tags) */
code.codefont
	{ font-family: Courier, monospace, serif }

/* Blue text references embedded in narrative */
font.fontblue
	{ color: #0000FF }

/* End of File */