h1{
  font-size: x-large;
  background-color:#4040C0;
  border-top: 1px solid #C0C0E0;
  border-left: 1px solid #C0C0E0;
  border-bottom: 1px solid #000040;
  border-right; 1px solid #0000040;
  color:white;
  padding:3px 1ex;
  margin: 0 0 1ex -1ex;
}

h2{
  font-size: large;
  background-color: #A0A0A0;
  border-top: 1px solid #E0E0E0;
  border-left: 1px solid #E0E0E0;
  border-bottom: 1px solid #202020;
  border-right; 1px solid #202020;
  color: white;
  padding: 3px 1ex;
  margin: 0 0 0 -1ex;
}

h5{
  margin: 0 1ex 0 0.5ex;
}

table.normal {
  border: 1px #C0C0C0 solid;
  border-collapse: collapse;
  margin: 1ex 1ex 1ex 1ex;
}

table.normal th,
table.normal td,
table.normal td.nowrap {
  border: 1px #C0C0C0 solid;
  padding: 0.3ex 1ex 0.3ex 1ex;
}

table.normal th {
  background: #F0F0F0;
  text-align: center;
  white-space: nowrap;
  color: black;
}

table.normal td {
  background: white;
  text-align: left;
  white-space: normal;
  color: black;
}

table.normal td.nowrap {
  background: white;
  text-align: left;
  white-space: nowrap;
  color: black;
}

div.section{
  margin:0.5ex 0 8ex 0ex;
  padding:0 0 0 2ex;
}

div.section div.section{
  margin:0.5ex 0 8ex 0ex;
  padding:0 0 0 2ex;
}

div.section div.section h1{
  font-size: large;
  background-color:#C0C0C0;
  color:white;
  padding:2px 1ex;
  margin:1ex 0 2ex -2ex;
}

div.subsection{margin:1ex 0 8ex 2ex;}

div.text{
  background-color:#F4FFFF;
  border-style:dotted;
  border-width:thin;
  border-color:gray;
  margin:0.5ex 0 0.5ex 2ex;
  padding:1ex;
}

pre.src{
  background-color:#F4FFFF;
  border-style:dotted;
  border-width:thin;
  border-color:gray;
  margin:0.5ex 1ex 2ex 2ex;
  padding:1ex;
}