div#main div.float {
    float: right;
    padding-right: 20px;
}

div#main div.float p {
    text-align: center;
    font-size: 0.8em;
    border: 0px;
    margin:  -0.2em;
    padding: 0em;
}

body {
    margin:0;
    padding:0;
    font: 13px verdana, arial, helvetica, sans-serif;
    color:#333;
    background-color:white;
}
h1 {
    margin: 0;
    padding:0;
    font: bold 1.2em sans-serif;
}

h2 {
    font: bold 1.50em sans-serif;
    padding: 0;
    margin: 0;
    border-bottom: 1px solid rgb(80%,75%,70%);
}

h3 {
    font: 1.33em sans-serif;
    padding: 0;
    margin: 0;
}

h4 {
    font: bold 1.11em sans-serif;
    padding: 0;
    margin: 0;
}

li {margin: 1em 2em 0.8em 1.4em;}




#main>p {margin:0px;}

a {
    color:#09c;
    text-decoration:none;
    font-weight:600;
    font-family:verdana, arial, helvetica, sans-serif;
}

a:link {color:#09c;}
a:visited {color:#07a;}
a:hover {background-color:#eee;}

#banner {
    margin:20px 0px 10px 0px;
    padding:17px 0px 10px 20px;
    border-style:solid;
    border-color:black;
    border-width: 1px 0px; /* top and bottom borders: 1px; left and right borders: 0px */
    line-height: 1em;
    background-color:#eee;

}


#main {
    margin: 0 1em 1em 14em;
    padding: 0;
    
}
div#main p {margin: 1em 2em 0.8em 1.4em;}

div#main h3 {padding: 0.5em 0 0 1em;}
div#main h4 {padding: 0.5em 0 0 1.2em;}

/* Bibtex page*/
.bibtex { 
    font: 0.8em sans-serif;
    padding: 0em 0em 0em 1em;
}



div#sidelinks {
    padding: 0; float: left;
    padding-top: 10px;
    width: 10em;
    margin: 0 0em 0 25px
}


div#sidelinks a { 
    display: block; 
    padding: 0.5em 1em 0.5em 1.2em;
    text-decoration: none;
    border: 1px solid;
    background-color:#eee;
    border:1px dashed #999;
    line-height:17px;

}
/*
  div#sidelinks a#navigation { 
  border: none;
  background: rgb(96%,95%,94%);
  }
  div#sidelinks a#navigation:hover { 
  color: rgb(11%,16%,66%); 

border-bottom-color: red;
border-top-color: rgb(69%,75%,85%);
background-color: rgb(90%,85%,81%);
}
*/
div#sidelinks h4 {
    font: 1em sans-serif;
    padding: 0;
    margin: 0;
    
}
div#sidelinks a:hover {
    color: rgb(11%,16%,66%); 
    border-bottom-color: rgb(69%,75%,85%);
    border-top-color: rgb(69%,75%,85%);
    background-color:#eee;
}


div#sidelinks a.level1 {
    padding: 0.3em 1em 0.3em 2em;
    font-size: 0.85em;
}

/* footer div */
div#footer {
    text-align: right;
    margin: 4em 2em 0 0;
    font-size: 0.85em;
}

div.code {
    border: 2px dotted;
    font-family: Courier, monospace;
    font-size: 1em;
    padding: 0.7em 0em 0.7em 4em;
    margin: 0.8em 3em 0.8em 2em;
    background-color: #eee;
}



/*bookmarks*/

div.bookmarklink{
    padding: 0.4em 2em 0.8em 1.4em;
}

div.bookmarklink a{
    display: block;
}

div.bookmarklink a:hover {
    color: rgb(11%,16%,66%); 
    border-bottom-color: rgb(69%,75%,85%);
    border-top-color: rgb(69%,75%,85%);
    background-color: #eee;
}

/*bookmark headers*/
div#header {
    border-style:solid;
    border-color:black;
    border-width: 1px 0px; /* top and bottom borders: 1px; left and right borders: 0px */
    line-height: 1em;
    margin:20px 0px 10px 0px;
    padding:17px 20px 10px 20px;
    background-color: #eee;
}

div#header h1 {margin-bottom: -1em}

div#header form {text-align:right;}

/*crumbs*/

div#bookmarkcrumbs{
    margin-bottom:0.7em;
    margin-top: 0.7em;
    margin-left: 20px;
    color: #eee;
}

/*form*/

input {border: 1px dotted #aaa;}

select {border: 1px dotted #aaaaaa;}