html {
   background: url('./bg_0.png') #eeeeee;
   padding: 0px;
   margin: 0px;
   font-family: verdana,helvetica,arial,sans-serif;
   min-height: 100%;
}

body {
   padding: 0px 0px 0px 0px;
   margin: 0px;
   background: url('./bg_body.png') repeat-x #bfbfbf;
   width: 50em;
   max-width: 90%;
   margin: 0px auto 0px auto;
   min-height: 100%;
}


#navigation {
   font-size: medium;
   margin: 0px;
   margin-right: 5%;
   padding: 0px;
   width: 15%;
   min-width: 135px;
   float: right;
}

#navigation ul {
   background: url('./bg_pages.png') repeat-x #0092ff 100% 100%;
   color: white;
   list-style: none;
   margin: 0px;
   padding: 10px;
}

#navigation ul li {
   margin: auto;
   padding: 0px;
   line-height: 190%;
}

#navigation ul li img {
   vertical-align: middle;
}


#h1 {
   background: url('./bg_shadow.png') repeat-y;
   padding-left: 10%;
   padding-right: 30%;
   border-right: solid 1px #666666;
   border-left: solid 1px #666666;
   color: #535353;
   min-height: 100%;
   padding-top: 6em;
   padding-bottom: 4em;
}


#h1 a {
   color: #a07000;
}

#h1 a:visited {
   color: #883300;
}


h1 {
   margin-top: 0px;
}



#abstract {
   margin: 3em auto 0em auto;
   font-size: 10pt;
   color: #535353;
}

#h1 *:last-child {
   margin-bottom: 0px;
}

.section p {
   text-align: justify;
   text-justify: auto;
   line-height: 160%;
}

#h2 {
   margin-top: 8em;
}

#h2 * {
   font-size: 10pt;
}

#h2 h2 {
   font-size: larger;
   margin-bottom: 2em;
}

#h2 h3 {
   margin-top: 3em;
}


#footer {
   background: url('./bg_footer.png') repeat-x #ff8000;
   border-right: solid 1px #666666;
   border-left: solid 1px #666666;
   color: black;
   font-size: 10pt;
}

#footer ul {
   margin: 0px;
   padding: 10px 0em 0.3em 0em;
   background: url('./bg_shadow.png') repeat-y;
   list-style: none;
   min-height: 30px;
}

#footer ul li {
   text-align: center;
   padding: 0px;
   vertical-align: bottom;;
}

a img {
   border: none;
}

.section > pre {
   background: white;
   padding: 0.3em;
   border: 1px solid #666666;
}



#top-topics {
   font-size: medium !important;
   margin: 0px;
   margin-bottom: 0px !important;
}

#top-topics + * {
   margin-top: 0.3em;
   font-size: 10pt;
}

#top-toc {
   margin-top: 4em;
}

#top-toc dt {
   margin-top: 1em;
   font-size: 130%;
   font-weight: bold;
}

#top-toc dd {
   margin-left: 0em;
   font-size: small;
}