body {
  background: white;
  margin: 5%;
  /*/*/ line-height: 1.5; /* */
}
h2 {
  font-size: large;
  margin: 2em 0em 0em 0em;
  padding: 0.2em 0.5em;
  border-width: thin;
  border-color: white;
  background-color: #99F;
}
h3 {
  margin: 1em 0em 0em 0em;
  padding: 0.2em 0.5em;
  border-style: solid;
  border-width: 0px 0px 0px 20px;
  border-color: #99F;
}
pre {
  color: maroon;
  overflow: auto;
  /*/*/ line-height: 1.2; /* */
}
code, tt { color: maroon }
em { font-style: normal; color: #F30 }
a:hover, a:focus, a:active { color: red }
a[name]:hover, a[name]:focus, a[name]:active { color: black }
img { border-style: none }
td, th { padding: 0.2em 0.7em }
.note {
  margin-left: 0em;
  padding-left: 1.5em;
  border-left: #FC3 solid 0.5em;
  /*/*/ line-height: 1.3; /* */
}
.left { float: left; margin: 1em 1em 1em 0em; }
.right { float: right; margin: 1em 0em 1em 1em; }
.old { background: #FFC; }