    #footer p { font: smaller monospace; color: gray; background: white; text-align: right; margin-right: 2em }

    /*.external:after { content: url(img/arrow.gif); position: relative; bottom: 0.5ex   }
    */

    #nav { background: #ddd; padding: 0.5ex }
    #subnav { background: #eee; padding: 0.5ex; font-size: smaller }
    
    a.external { font-style: italic }
    a.external:hover { background: #ddd }
 
    body { font-family: Optima, Palatino, sans-serif }

    p, address, ul, dl, table, pre { margin-left: 5%; margin-right: 10% }

    dd p { margin-top: 0; margin-left: 0%; margin-right: 0% }

    p, dd, pre { margin-bottom: 1em }
    
    dt { font-weight: bold }

    address { font-size: small; font-style: normal }

    a img { border: none }
 
 
    ul, li { padding-left: 0 }
    ul li { list-style: square }

    ul.biglinks li { list-style: none; font-size: 120%; font-weight: bold }
    ul.biglinks li p { font-weight: normal; font-size: 83.33% }

    a { text-decoration: none }
    a:hover { text-decoration: underline }

    .centered { text-align: center }

    h1, h2 { color: navy; background: white }
    h1 { font-size: larger }
    h2 { font-size: medium }

    pre { background: #ffb; 
                padding: 1ex 1em 1ex 1em; 
                font: smaller monospace
             }
        
    p.license { font-size: small }

    span.ident {}
    span.punct { color: #060 }
    span.constant { color: #00c; font-weight: bold }
    span.ident { color: black }
    span.string { color: #830 }
    span.number { color: #808 }
    span.keyword { color: #442; font-weight: bold }
    
