body {
 margin:     10px;
 margin-top: 30px;
 margin-bottom: 100px;
}

table, tr, td {
  font-size: inherit;
  font-family: inherit;
  font-weight: inherit;
}

div {
 display: block;
}

div.none {
 display: inline;
}

div.navigation {
  font-size: medium;
 position: fixed;
 right: 10px;
 top: 0;
 padding-left: 5px;
 padding-bottom: 5px;
 padding-right: 5px;
 border-left: outset black 4px;
 border-bottom: outset black 4px;
 border-right: outset black 4px;
 background-color: #ffffc0;
 text-align: center;
 font-weight: bold;
 font-family: sans-serif;
}

div.title {
  font-size: 300%;
  font-weight: bold;
  text-align: center;
  margin-top: 20px;
  margin-bottom: 20px;
  border-top: solid black 5px;
  border-bottom: solid black 5px;
 width: 100%;
  background-color: #ffffc0;
}

div.smalltitle {
 display: inline;
 font-weight: bold;
 background-color: #ffffc0;
 padding: 3px;
}

div.mediumtitle {
 display: block;
 text-align: left;
 font-weight: bold;
 font-size: 150%;
 margin-top: 10px;
 margin-bottom: 5px;
}

div.main {
  font-size: 150%;
 width: 100%;
  font-weight: bold;
  /* width: 80%;
     margin-left: 10%; */
}

div.shell {
  font-family: monospace;
  font-weight: bold;
 border: solid #800000 3px;
  background-color: #ffc0c0;
  margin-top: 10px;
  margin-bottom: 10px;
 padding: 7px;
  white-space: pre;
 overflow: auto;
}

div.code {
  font-family: monospace;
  font-weight: bold;
  margin-top: 10px;
  margin-bottom: 10px;
 padding: 7px;
  background-color: #d0d0d0;
  white-space: pre;
 overflow: auto;
}

div.inlinecode {
 display: inline;
 font-family: monospace;
 font-weight: bold;
}

div.centertext {
 text-align: center;
  background-color: #ffffc0;
  font-size: 120%;
  font-weight: bold;
 border: solid black 1px;
 padding: 10px;
  margin-top: 10px;
  margin-bottom: 10px;
}

div.image {
  text-align: center;
}

div.em {
 display: inline;
 background-color: #ffc0c0;
 border: solid #800000 1px;
}

div.em2 {
 display: inline;
 background-color: #c0c0ff;
 border: solid #000080 1px;
}

div.quotation {
 width: 60%;
 margin-left: 20%;
 margin-top: 10px;
 margin-bottom: 10px;
 padding: 10px;
 text-align: left;
 white-space: pre;
 overflow: visible;
 background-color: #e0e0e0;
 border: solid black 1px;
}

div.attrib {
  margin-top: 15px;
  text-align: right;
  font-style: italic;
}

table.comparison td {
 spacing: 0px;
 padding: 5px;
 border: 2px solid black;
}

table.comparison td.title {
  background-color: #ffc0c0;
}