.navtext {
	font-family: Verdana, Arial, Helvetica, sans-serif;
	font-size: 12px;
	line-height: 17px;
}
.text {
	font-family: Verdana, Arial, Helvetica, sans-serif;
	font-size: 12px;
	line-height: 20px;
}
.header {
	font-family: Arial, Helvetica, sans-serif;
	font-size: 20px;
	font-weight: bolder;
	border-bottom-style: solid;
	border-bottom-color: #990000;
}.headtext {
	font-family: Verdana, Arial, Helvetica, sans-serif;
	font-size: 14px;
	font-weight: bold;
}
.compiler_text {
	font-family: "Courier New", Courier, monospace;
	font-size: 15px;
	font-weight: normal;
}