h1, h2, h3, h4, h5 {
  font-family: Verdana,Arial,sans-serif;
  text-align: left;
}

a {
  font-family: Verdana,Arial,sans-serif;
  font-size: 95%;
  text-decoration: none;
}

span.urlpart {
  font-family: Verdana,Arial,sans-serif;
  font-size: 95%;
}

span.para {
  font-family: Verdana,Arial,sans-serif;
  font-size: 95%;
}

table.header {
  font-family: Verdana,Arial,sans-serif;
  font-size: 85%;
  border-top-width: thin;
  border-top-style: solid;
  border-top-color: rgb(230,230,230);
  border-bottom-width: thin;
  border-bottom-style: solid;
  border-bottom-color: rgb(230,230,230);
  margin-bottom: 2ex;
  width: 100%;
  table-layout: fixed; /* ?? */
}

body {
  font-family: Georgia,"Times New Roman",Times,serif;
}

a.extern:link {
  color: rgb(25,76,0);
}

a.ref:link {
  color: rgb(76,0,0);
}

a.ref:visited {
  color: rgb(76,0,0);
}

span.maddr {
  color: rgb(25,76,0);
}

span.normal {
  font-style: normal;
  font-weight: normal;
}

.new {
  margin-top: 4ex;
  padding-top: 0ex;
  background-color: rgb(230,242,255);
}

.updated {
  margin-top: 4ex;
  padding-top: 0ex;
  background-color: rgb(230,242,255);
  margin-bottom: 2ex;
}

/*
p:first-child {
  text-indent: 0px;
}
*/

ul li {
  list-style-type: circle;
}

ul li li {
  list-style-type: circle;
}

body {
  margin-left: 50px;
  margin-right: 50px;
/* text-align: justify; */
  max-width: 800px;
}

h1, h2, h3, h4, h5, p {
  padding-top: 0px;
  padding-bottom: 0px;
  padding-left: 5px;
  padding-right: 5px;
}

p {
  margin-top: 0px;
  margin-bottom: 0px;
  text-indent: 1em;
}

p.index {
  text-align: center;
  text-indent: 0px;
}

p.first {
  text-indent: 0px;
}

p.separate {
  margin-top: 1ex;
  text-indent: 0px;
}

p.finalnote {
  margin-top: 1ex;
  text-indent: 0px;
}

ol, ul {
  padding-right: 5px;
}

li p {
  text-indent: 0px;
  padding-left: 0px;
  padding-right: 0px;
  margin-left: 0px;
  margin-right: 0px;
}

.title {
  text-align: center;
}

h4.author {
  text-align: center;
}

p.para {
  text-indent: 0px;
  margin-top: 1em;
}  

span.para {
  font-weight: bold;
  margin-right: 2ex;
}

h5 {
  font-size: 1em;
  display: run-in;
}


div.headertable {
  margin-left: 0.3em;
  margin-right: 0.3em;
  padding-left: 0px;
  padding-right: 0px;
}

div.verbatim {
  margin-top: 1ex;
  margin-bottom: 1ex;
}

td {
  vertical-align: baseline;
}

td.hleft {
  text-align: left;
/*  width: 20%;  */
}

td.hright {
  text-align: right;
  width: auto;
}