body  {
  margin-left: 3%;
  margin-right: 3%;
  margin-top: 4em;
  margin-bottom: 4em ;
  font-family: sans-serif;
  color: black;
  background: white;
}
h1.title { 
  text-align: center;
}
p { 
  text-align: justify;
}
div.informaltable {  
  margin-left: 2%;
}
div.informalexample { 
  margin-left: 0%;
}
table {
  #border: 1px solid rgb(100,100,100);
  border-collapse: collapse;
  color: black;
  background: rgb(240,240,240);
}
table.simplelist {
  margin-left: 2%;
  border: 0px;
  background: white;
}
td { 
  padding: 4px;
}
pre {
  color: black;
  background: rgb(240,240,240);
  border: 1px solid rgb(100,100,100);
  padding: 6px;
}

.informaltable td { 
  padding-right: 2em;
  background: white;
  border: 0px;
}
span.application { 
  font-weight: bold;
}
.dtdtopcmnt {  
  margin-left: 6%;
  margin-right: 6%;
}
.dtdeltname {  
  font-weight: normal;
}
.dtdelttitle, .entdeftitle {  
  text-align: left;
  font-size: 130%;
  font-style : normal;
  font-weight : normal;
  color: #a80000;
}
.dtdeltdesc {  
  margin-left: 6%;
  margin-right: 6%;
  text-align: justify;
}
.dtdeltdef { 
  font-size: 60%;
}