/* pre { font-family: monospace; } */    /* recommended at http://www.w3.org/MarkUp/Guide/Style, */
                                         /* but confuses Mozilla */
body { color: black; background-color: white; background-repeat: no-repeat }
p.vvlarge { margin-top: 6ex; margin-bottom: 0 }
p.vlarge { margin-top: 4ex; margin-bottom: 0 }
p.large { margin-top: 3ex; margin-bottom: 0 }
p { margin-top: 2ex; margin-bottom: 0 }
p.small { margin-top: 1ex; margin-bottom: 0 }
p.tiny { margin-top: 0.5ex; margin-bottom: 0 }
p.hdr { margin-top: 3ex; margin-bottom: 0 }
p.subhdr { margin-top: 2.5ex; margin-bottom: 0 }
p.right { text-align: right; margin-right: 1ex }
p.scrollspace { margin-top: 100em; margin-bottom: 0 }
/* tbody { text-align: left; vertical-align: baseline } */
ul.lessindent { padding-left: 4ex }
img.lower { vertical-align: -3ex }
code { padding-left: 0.5ex; padding-right: 0.5ex }
.smallfont { font-size: smaller }
.baseline { vertical-align: baseline }
.notop { margin-top: 0 }
.nobottom { margin-bottom: 0 }