ul.nested {
   margin-left : 2em; 
   list-style : none; 
}


ul.linklist {
   margin-bottom : 2em; 
   margin-left : 0; 
   list-style : none; 
}


tr {
   text-align : left; 
   margin-top : 0.2em; 
   margin-bottom : 0.2em; 
   margin-left : 1em; 
   padding : 4px; 
   border-width : 1px; 
   border-style : solid; 
   border-color : gray; 
}


td {
   text-align : left; 
   margin-top : 0.2em; 
   margin-bottom : 0.2em; 
   margin-left : 1em; 
   padding : 4px; 
   border-width : 1px; 
   border-style : solid; 
   border-color : gray; 
}


pre.example {
   font-size : 90%; 
   font-family : monospace; 
   margin-top : 0.5em; 
   margin-bottom : 1.5em; 
   margin-left : 2%; 
}


p {
   margin-top : 0.2em; 
   margin-bottom : 1em; 
} p.cr {
   font-size : 80%
}

li {
   margin-top : 1em; 
   margin-bottom : 1em; 
}


img {
   border-width : 0; 
   border-style : none; 
   border-color : inherit; 
   float : right; 
}


h5 {
   font-style : italic; 
   font-weight : bold; 
   font-size : 80%; 
   margin-top : 1.2em;
   color : #000099; 
   margin-bottom : 0.2em; 
}


h4 {
   font-style : italic; 
   font-weight : bold; 
   font-size : 88%; 
   color : #000099; 
   margin-top : 2.5em; 
   margin-bottom : 0.4em; 
}


h3 {
   font-style : italic; 
   font-weight : bold; 
   font-size : 100%; 
   color : #000099; 
   letter-spacing : 0.05em; 
   margin-top : 2.5em; 
   margin-bottom : 1em; 
}


h2 {
   font-style : normal; 
   font-weight : bold; 
   font-size : 150%; 
   color : #000099; 
   letter-spacing : 0.05em; 
   margin-top : 3em; 
   margin-bottom : 1em; 
}


h1 {
   font-style : normal; 
   font-weight : bold; 
   font-size : 190%; 
   color : #000099; 
   margin-top : 3em; 
   margin-bottom : 1em; 
}


em {
   font-style : italic; 
   font-size : 100%; 
}


dt {
   font-size : 100%; 
   margin-top : 0.8em; 
   margin-bottom : 0.2em; 
   margin-left : 2%; 
}


div.sidebar {
   background-color : #ffffff; 
}


div.notice {
   font-style : normal; 
   font-weight : normal; 
   font-size : 95%; 
   color : #000033; 
   background-color : #ffffff; 
   margin : 1em 1em 1em 0; 
   padding : 0.5em; 
   border-width : 2px; 
   border-style : solid; 
   border-color : #005a9c; 
}


dd.newmandatory {
   font-style : italic; 
   font-size : 80%; 
   margin-top : 0.1em; 
   margin-left : 4%; 
}


dd.deprecated {
   font-style : italic; 
   font-size : 80%; 
   margin-top : 0.1em; 
   margin-left : 4%; 
}


dd {
   font-size : 100%; 
   margin-top : 0.1em; 
   margin-left : 4%; 
}


body {
   font-style : normal; 
   font-weight : normal; 
   font-family : arial, verdana, sans-serif; 
   margin-right : 5%; 
   margin-left : 5%; 
}


a:hover {
   color : #ff0000;
}


a {
   color : #000099;
   text-decoration: none;
}