/* If I say "font-size: medium;", which is what I'd like to do, I get
wildly different results in netscape and ie. Sigh. So I have to resort to
the following crap. */

/* medium */
body, li, p, DIV.abstract {
    font-size: 12pt;
}

/* large */
h1, h2 {
    font-size: large;
}

/* x-large */
P.pagetitle {
    font-size: x-large;
}

/* small */
small.comment, SPAN.reveal, P.index, pre {
    font-size: small;
}

/* x-small */
p.bookmark {
    font-size: 8pt;
}

body {
    font-family: Helvetica, sans-serif;
    background: #bbffdd;
    color: #000000;
}

img.right {
    float: right;
}


LI {
/*    font-family: Arial, Helvetica, sans-serif;*/
}

A {
    background: transparent;
}

A:link, A:visited, A:active  {
    background-color: transparent;
}

A:link {
    color: blue;
}

A:visited {
    color: #800040;
}

A:active {
    color: red;
}


HR {
    clear: left;
}

H1, H2, H3, P.pagetitle {
    background-color: transparent;
    color: #006020;
    clear: left;
}

H1 {
    font-weight: bold;
}

H2, H3 {
    font-weight: normal;
}


P {
}

P.pagetitle {
    font-weight: bold;
}

pre {
    font-family: Courier, Monospace;
}

div.strike {
    text-decoration: line-through;
}

OL.loweralpha {list-style-type: lower-alpha }