BODY { 
       background-color: #FFFFFC; 
       font-family: DejaVu Sans, Verdana, Arial, Helvetica, sans-serif;
       margin: 3%;
     }

H1   {
         display: block;
         font-family: DejaVu Sans, Verdana, Arial, Helvetica, sans-serif;
         font-size: 120%;
         margin-top: 0.8em;
         margin-bottom: 0.8em;
     }

H2   {
         display: block;
         font-family: DejaVu Sans, Verdana, Arial, Helvetica, sans-serif;
         font-size: 110%;
         margin-top: 1.5em;
         margin-bottom: 0.67em;
     }
     
PRE { background-color:#DDDDDD; 
       padding-left: 1cm;
       padding-bottom: 1em;
     }

div.gfn-info {
    width: 80em;
}

div.gfn-help {
    font-family: DejaVu Sans Mono, Lucida Console, Consolas, Courier, monospace;
}         

.footnote {
   font-size: 70%
}