body { font-family: Arial, Tahoma, sans-serif; background-color: #f0f8ff; }

h3 { margin-left: 22px; }

table.menu { background-color: #3399cc; padding: 1px; }
td.right { text-align: right; }

a.menuH { color: white; text-decoration: none; font-weight: bold }
a.menuH:hover { color: #3399cc; background-color: white; }
a.title { font-weight: bold; text-decoration: none; color: black; }
a.title:hover { text-decoration: underline; }

pre { font-family: Courier, monospace; color: #4682b4; }

/*
.source, .JavaScript, .output { border: thin solid black; }
*/

a.smallBlackLink {
  font-size: 60%;
  font-weight: bold;
  color: black;
  text-decoration: none;
}

span.red {color: red}