spacer {
	display: block;
	clear: both;
	content: "";
	height: 0px;
	line-height: 0px;
}

div.topbar {
        background:     #4271FF;
        margin:         0px;
        padding-top:    5px;
        padding-right:  15px;
        padding-left:   15px;
        padding-bottom: 5px;
        border-bottom:  1px solid #000000;
}

div.topbar2 {
        background:     #FFD042;
        padding-top:    5px;
        border-top:     1px solid #000;
        border-bottom:  1px solid #000;
}

div.topbarname {
        font-family:    Curier, Curier New, Monospace, Verdana, Arial, Helvetica, monospace;
        font-weight:    bold;
        font-size:      20px;
        color:          #fff;
}

a.goindextop {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        font-size:      20px;
        color:          #fff;
        float:          right;
	padding-left:   2em;
	padding-right:  2em;
}
a.goallprinttop {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        font-size:      20px;
        color:          #fff;
        float:          right;
	padding-left:   2em;
	padding-right:  2em;
}

div.syntax {
        background:     #E6E6E6;
        margin:         10px;
        padding:        10px;
        border:         1px solid #000;
        font-family:    Curier, Curier New, Monospace, Verdana, Arial, Helvetica, monospace;
}

div.syntaxcat {
        padding:        3px;
        text-align:     center;
        font-family:    Verdana, Arial, Helvetica, sans-serif;
}

div.syntaxspec {
        display:        block;
        padding:        5px;
        border-left:    1px dotted #aaa;
}

div.syntaxinfo {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        float: left;
}

div.syntaxtype {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        text-align:     right;
}

span.syntaxname {
        font-weight:    bold;
        margin-right:   1ex;
        margin-left:    2ex;
}

span.syntaxargname {
        font-style:     italic;
        margin-left:    1ex;
        margin-right:   1ex;
}

span.syntaxargnote {
        font-style:     italic;
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        font-size:      x-small;
        
}

span.syntaxresult {
        margin-left:    1ex;
}

div.syntaxarginfo {
        border-left:    1px dotted #aaa;
        padding:        5px;
        font-family:    Verdana, Arial, Helvetica, sans-serif;
}

table.syntaxargtab {
        padding-left:   2ex;
}

td.syntaxargdesc {
        font-family:    serif;
        padding-left:    2em;
}


div.botbar2 {
        background:     #FFD042;
        padding-top:    3px;
        border-top:     1px solid #000;
        border-bottom:  1px solid #000;
}

div.botbar {
        background:     #4271FF;
        margin:         0px;
        padding-top:    5px;
        padding-right:  15px;
        padding-left:   15px;
        padding-bottom: 5px;
        border-bottom:  1px solid #000000;
}

a.hyperspec {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        font-size:      16px;
        color:          #fff;
}

span.hyperspecname {
        font-family:    Curier, Curier New, Monospace, Verdana, Arial, Helvetica, monospace;
        font-weight:    bold;
        font-size:      16px;
}

a.goindexbot {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        font-size:      16px;
        color:          #fff;
        float:          right;
}

/* index styles  */

div.spacer {
	display:        block;
	clear:          both;
	content:        "";
	height:         0px;
	line-height:    0px;
        padding-top:    3px;
}

div.categorycontainer {
        border:         1px solid #000;
        margin-left:    15px;
        margin-right:   15px;
        margin-top:     7px;
        margin-bottom:  2px;
        width:          90%;
        float:          left;
}

div.categoryinside {
        padding:        2px 5px 5px 5px;
        background:     #f4f4f4;
}

div.categorydesc {
        font-family:    Verdana, Arial, Helvetica, sans-serif;
        padding:        2px 5px 2px 5px;
        border-bottom:  1px dotted #aaa;
}

a.categorysymbol {
        font-family:    Curier, Curier New, Monospace, Verdana, Arial, Helvetica, monospace;
        font-size:      16px;
        padding-right:  1ex;
}

.symbolnotdefined {
        background:     #faa;
        display:        none;
}

.catcol_math {
        background:     #66D9FF;
        color:          #000;
}

.catcol_control {
        background:     #8CFF66;
        color:          #000;
}

.catcol_cons {
        background:     #FFD966;
        color:          #000;
}

.catcol_io {
        background:     #E699FF;
        color:          #000;
}
.catcol_other {
        background:     #FFB399;
        color:          #000;
}
.catcol_sequence {
        background:     #E0E000;
        color:          #000;
}

