[2] | 1 | /* pre { font-family: monospace; } */ /* recommended at http://www.w3.org/MarkUp/Guide/Style, */ |
---|
| 2 | /* but confuses Mozilla */ |
---|
| 3 | body { color: black; background-color: white; background-repeat: no-repeat } |
---|
| 4 | p.vvlarge { margin-top: 6ex; margin-bottom: 0 } |
---|
| 5 | p.vlarge { margin-top: 4ex; margin-bottom: 0 } |
---|
| 6 | p.large { margin-top: 3ex; margin-bottom: 0 } |
---|
| 7 | p { margin-top: 2ex; margin-bottom: 0 } |
---|
| 8 | p.small { margin-top: 1ex; margin-bottom: 0 } |
---|
| 9 | p.tiny { margin-top: 0.5ex; margin-bottom: 0 } |
---|
| 10 | p.hdr { margin-top: 3ex; margin-bottom: 0 } |
---|
| 11 | p.subhdr { margin-top: 2.5ex; margin-bottom: 0 } |
---|
| 12 | p.right { text-align: right; margin-right: 1ex } |
---|
| 13 | p.scrollspace { margin-top: 100em; margin-bottom: 0 } |
---|
| 14 | /* tbody { text-align: left; vertical-align: baseline } */ |
---|
| 15 | ul.lessindent { padding-left: 4ex } |
---|
| 16 | img.lower { vertical-align: -3ex } |
---|
| 17 | code { padding-left: 0.5ex; padding-right: 0.5ex } |
---|
| 18 | .smallfont { font-size: smaller } |
---|
| 19 | .baseline { vertical-align: baseline } |
---|
| 20 | .notop { margin-top: 0 } |
---|
| 21 | .nobottom { margin-bottom: 0 } |
---|