/* local style sheet */

pre {
    padding: 1em;
    border: 1px dashed #2f6fab;
    color: Black;
    background-color: #f9f9f9;
    line-height: 1.1em;
}
h3 {
  font-family: verdana, helvetica, arial, sans-serif;
  font-size:14pt;
  margin-top:20pt;
  margin-bottom:14pt;
  color:#808080;
}
/*.example {
    overflow: auto;
    max-width: 100%;
    padding: 1em;
    border: 1px dashed #2f6fab;
    color: Black;
    background-color: #f9f9f9;
    line-height: 1.1em;
    font-size: 9pt;
}*/