/* style.css a minimal style sheet */
body 
{
    margin-left: 3em;
    margin-right: auto;
    max-width: 50em;
}

img.banner
{
    margin-left: -3em;
}

pre.code {
    margin-left: 3em;
    font-size-adjust: 0.65;
    font-family: monospace;
    margin-top: 0.2ex;
    margin-bottom: 0.2ex;
}
span.code {
    font-size-adjust: 0.65;
    font-family: monospace;
}
span.code:before {
    content: "'";
}

span.code:after {
    content: "'";
}

div.pltbox {
    display: inline-block;
    horizontal-align: center;
    vertical-align: top;
    font-size-adjust: 0.5;
    margin: 10px 10px 10px 10px;
    border: solid;
    padding: 3px 3px 3px 3px;
}

p.label {
    margin: 3px 3px 3px 3px;
}