body { font-family: Georgia, serif;
       line-height: 1.3;
       padding-left: 5em; padding-right: 1em;
       padding-bottom: 1em; max-width: 60em; }
table { border-collapse: collapse }
span.roman { font-family: century schoolbook, serif; font-weight: normal; }
h1, h2, h3, h4, h5, h6 { font-family:  Helvetica, sans-serif }
h4 { margin-top: 2.5em; }
dfn { font-family: inherit; font-variant: italic; font-weight: bolder }
var { font-variant: slanted; }
td  { padding-right: 1em; padding-left: 1em }
sub { font-size: smaller }
.node { padding: 0; margin: 0 }
dd { padding-top: 1em; padding-bottom: 2em }
pre.example {
  font-family: monospace;
  background-color: #E9FFE9; border: 1px solid #9D9;
  padding-top: 0.5em; padding-bottom: 0.5em; }
a:link { color: #383; text-decoration: none; padding: 1px 2px 1px 2px; }
a:visited { color: #161; text-decoration: none; padding: 1px 2px 1px 2px; }
a:hover { color: #161; text-decoration: none; padding: 1px 1px 1px 1px; border: 1px solid #666; }
a:focus { color: #161; text-decoration: none; padding: 1px 2px 1px 2px; border: none; }