html, body {
	padding: 0px;
	margin: 0px;
	border: 0px;
}

body {
	font-family: Verdana, sans-serif;
	font-size: 0.83em;
	background-color: #CAD0D9;
	color: black;
}

h1, h2, h3 {
	font-family: Garamond, Georgia, 'Times New Roman', serif;
}
h1 { color: #3F589F; font-size: 22pt; margin-left: -0.8em; }
h2 { color: #1E637F; font-size: 17pt; margin-left: -0.7em; }
h3 { color: #1A4364; font-size: 14pt; margin-left: -0.4em; }

a:link      { color: #2A4375 }
a:visited   { color: #2E80A0 }
a:hover     { color: #A7A84A; text-decoration: none }
a:active    { color: #888888 }
/* a img       { border: none; } */

form input[type="text"] {
	border: solid 1px gray;
}

li { margin-top: 0.5em; margin-bottom: 0.5em; }

pre, code, tt {
	/* These seem useless but it's to get around the Firefox lameness of
	making the font here really small. */
	font-family:  'Courier New', monospace;
	font-size: 105%;
	font-style: normal;
	line-height: normal;
}

pre, code {
	border: 1px #808080 dotted;
}

pre.code, code {
	background-color: #fbf8d1;
}

pre.code i.var, code i.var {
	font-weight: normal;
}

code {
	padding: 0em 0.2em;
}

pre { 
	padding: 0.2em;
}

div#mainbody {
	background-color: white;
	padding: 2em 3em;
	width: 75%;
	max-width: 60em;
	margin-left: auto;
	margin-right: auto;
	margin-bottom: 30px;
	border-left: 0.1em solid #999999;
	border-right: 0.1em solid #999999;
	border-bottom: 0.1em solid #999999;
}

div#topbanner, #toplinks, div#toplinksbottom {
	margin: 0px;
}

div#topbanner {
	background-color: #717FBE;
	background-image: url('/images/tux.jpg');
	background-repeat: no-repeat;
	background-position: top left;
	padding-left: 3.5em;
	height: 100px;
}
/* Sons of Suckerfish */
#toplinks {
	background-color: #3E487F;
	color: white;
	text-align: center;
	border-top: 2px #506090 solid;
	border-bottom: 1px #626b9c solid;
	height: 2em;
}

#toplinks ul {
	list-style: none;
	padding: 0px;
	margin: 0px;
	line-height: 1em;
}

#toplinks ul#toplinkslist {
	margin-left: auto;
	margin-right: auto;
	/* IE: center links in middle of page */
	text-align: center;
	/* update to number of links */
	/* IE: needs to be bigger than n*width because IE sucks */
	width: 35.8em;
}

#toplinks li {
	width: 7em;
	float: left;
	position: relative;
	margin: 0px;
	padding: 0px;
}

#toplinks li ul {
	display: none;
	left: -999em;
	position: absolute;
	top: 100%;
	left: 0;
	/* padding: 0.05em;
	background-color: #5E689F; */
	border: 1px solid #7780A0;
}

#toplinks li ul ul {
	/* li vertpadding (0.5em + 0.5em)
	   + #toplinks ul line-height (1em)
	   + #toplinks li ul.droplinks li a vertborder (0.05em)
	   + #toplinks li ul vertpadding + vertborder (0 + 0.08em)
	   - ???
	   = 1.95em
	*/
	margin-top: -1.95em;
	margin-left: 14em;
}

#toplinks li li {
	display: block;
	/* IE: kill vertical space between li's */
	float: left;
	background-color: #3E487F;
	width: 14em;
}

#toplinks a {
	display: block;
}

#toplinks li:hover ul, #toplinks li.iefakehover ul {
	display: block;
	left: 0;
}

#toplinks li:hover ul ul, #toplinks li.iefakehover ul ul {
	display: none;
	left: -999em;
}

#toplinks li:hover ul, #toplinks li li:hover ul, #toplinks li.iefakehover ul, #toplinks li li.iefakehover ul {
	display: block;
	left: 0;
}

#toplinks ul li a {
	color: white;
	font-family: Verdana, sans-serif;
	font-weight: bold;
	text-decoration: none;
	font-size: 115%;
	padding: 0.4em 0px;
	width: 100%;
}

#toplinks li ul.droplinks li a {
	font-weight: normal;
	font-size: 1em;
	border-top: 1px solid #455389;
}

#toplinks li ul.droplinks li:first-child a {
	border-top: none;
}

/* Highlights links up the tree */
#toplinks li:hover > a {
	background-color: #596A96;
}

#toplinks a:hover {
	background-color: #596A96;
}

#toplinks a:active {
	background-color: #99AAC0;
}

div#toplinksbottom {
	background-color: #b0b5cf;
	/* This makes IE6 not draw a whole line for this element. */
	line-height: 1px;
	border-top: 1px #8a91b8 solid;
	border-bottom: 1px #cad0d9 solid;
}

div#topright {
	float: right;	
	color: #F2F2F2;
	padding-left: 1em;
	padding-right: 1em;
	margin-top: 15px;
	text-align: right;
}

#toprightlinks {
	margin-top: 6px;
	padding-top: 0px;
	margin-right: 2em;
}

#toprightlinks a, #toprightlinks a:link, #toprightlinks a:visited {
	color: white;
	text-decoration: none;
}

#toprightlinks a:hover {
    text-decoration: underline;
}

form#searchbox {
	display: inline;
	margin-top: 8px;
	padding-top: 0px;
	margin-right: 1em;
}

div#footer {
	color: #999999;
	font-size: 0.85em;
	font-style: italic;
	margin-top: 2.5em;
	border-top: 0.05em solid gray;
}

#toctitle {
	text-align: center;
	margin: 0.5em 0em;
	padding: 0em;
}

#toc {
	border: 0.05em solid gray;
	background-color: #F0F0F0;
	padding: 0em 1.5em;
	float: right;
	margin: 1em;
}

#toc td, #toc tr {
	padding: 0em;
}

#toc ol {
	margin: 0em;
}

ol.toc1 {
	list-style-type: decimal;
}

ol.toc2 {
	list-style-type: lower-alpha;
} /* There's also lower/upper-roman