a.termdef {
#  color: #850021;
  font-style: italic;
}

a.termref:visited, a.termref:link {
  font-family: sans-serif;
  font-style: normal;
  color: black;
  text-decoration: none
}

dt {
  font-weight: bold;
}

div.exampleOuter {
   border: 4px double gray;
   margin: 0em;
   padding: 0em;
}

div.exampleInner {
   color: black;
   /* mauve */
   background-color: #efeff8;
   border-top-style: double;
   border-top-color: #d3d3d3;
   border-bottom-width: 4px;
   border-bottom-style: double;
   border-bottom-color: #d3d3d3;
   padding: 4px;
   margin: 0em;
}

div.exampleInner pre {
  margin-left: 0em;
  margin-top: 0em;
  margin-bottom: 0em;
  font-family: monospace;
  /* font-size: smaller */
}

div.preExample {
  margin-left: 0em;
  margin-top: 0em;
  margin-bottom: 0em;
  font-family: monospace;
  /* font-size: smaller */
}

div.exampleLabel {
  align: center;
}