div.displaycode {margin-left: 40px; font-family: Courier New,Courier,monospace; font-size: 12pt}
div.indent {margin-left: 40px;}
div.contents {text-align: center;}
hr.normal {width: 100%; height: 2px;}
h1.normal {color: black; background-color: lightgrey;}
span.sans {font-family: Helvetica,Arial,sans-serif; font-size: 13pt}
span.italic {font-style: italic;}
span.code {font-family: Courier New,Courier,monospace; font-size: 12pt}
span.underconst {font-style: italic; color: rgb(153, 51, 0);}