body {
    max-width: 900pt;
    background-color: #fff;
    margin: 10pt;
}

body, p, td {
    font-size: 14pt;
    line-height: 18pt;
}

h1 {
    background: linear-gradient(rgba(128,207,216,0.6), rgba(127,202,147,0.45));
    border: thin solid gray;
    border-radius: 5px;
    margin-top: 10pt;
    padding: 15pt;
    padding-left: 10pt;
    margin-left: -2pt;
    font-size: 24pt;
}

h2 {
    border-bottom: medium solid gray;
    margin-top: 20pt;
    margin-bottom: 15pt;
    padding-bottom: 6pt;
    margin-left: -2pt;
    font-size: 16pt;
}

code {
    font-size: 14pt;
}

.example {
    font-size: 12pt;
    margin-left: 30pt;
    margin-right: 30pt;
    padding: 10pt;
    border: thin dotted gray;
    border-radius: 5px;
    font-family: monospace;
    background-color: #eee;
}

.navigation {
    font-size: 120%;
    margin-bottom: 30pt;
}

.navigation a {
    text-decoration: none;
    border: thin solid gray;
    border-radius: 5px;
    margin-right: 4pt;
    padding: 4pt 6pt;
    color: darkblue;
    background-color: lightblue;
}

.navigation a:hover {
    color: darkred;
}



.subtitle {
    font-size: 110%;
}

.indent {
    margin-left: 10pt;
}