body { border-width: 0 2em 0 2em; border-color: rgb(200,252,255);
       border-style: solid; padding: 1em;
       color: black; background: white; }
h1 { color: rgb(0,28,138); }
h2 { color: rgb(0,26,128); }
h3 { color: rgb(0,24,118); }
table.end { background: rgb(255,255,235); margin-top: 0.1em; font-size: 80%; }
div.example { background: rgb(250,240,200); 
       padding: 0.1em 0.5em 0.1em 0.5em; border: none; 
       font-family: sans-serif; }
table.std { background: rgb(255,255,235); }