body {font-family: "Helvetica", "Arial", sans-serif}
pre {
 margin: -1ex 0;
 border-width: thin;
 border-color: #AAAAAA;
 border-style: dotted;
 padding: 1em 0 0 0;
 background-color: #EEEEEE}
i {font-family: "Times-Roman", "Times New Roman", serif}