/* ################################################################ */
/* Settings for HTML elements                                       */
/* ################################################################ */

h1 { 
  color: #564e71;
}

body { 
  padding: 0px;
  margin: 0px;
  font-family: sans-serif;
  font-size: 12px;  
}

/**********************************************************************/
/* Settings for list (ol, dl, ...) elements                           */
/**********************************************************************/

.variablelist dl dt { 
  margin-top: 10px;
}

.variablelist dl dd p { 
  margin-top: 0px;
}

/*********************************************************************/
/* Settings for the style classes used by website                    */
/*********************************************************************/

.webpage { 
  margin-right: 5%;
}

.title { 
  color: #564e71;
}

/*********************************************************************/
/* Settings used for the navigation                                  */
/*********************************************************************/

SPAN.curpage {
  color: #3b3bf1;
  font-weight: bold;
}

SPAN.curpage A { color: #000000; }
SPAN.curpage A:link { color: #000000; }
SPAN.curpage A:visited { color: #000000; }

SPAN.toplevel A { color: #000000; }
SPAN.toplevel A:link { color: #000000; }
SPAN.toplevel A:visited  { color: #000000; }

SPAN.otherpage { color: #000000; }
SPAN.otherpage A { color: #000000; }
SPAN.otherpage A:link { color: #000000; }
SPAN.otherpage A:visited { color: #000000; }

SPAN.descendant A { color: #000000; }
SPAN.descendant A:link { color: #000000; }
SPAN.descendant A:visited { color: #000000; }

SPAN.ancestor A { color: #000000; }
SPAN.ancestor A:link { color: #000000; }
SPAN.ancestor A:visited { color: #000000; }

SPAN.shrink1 { font-size: 80%; }
SPAN.shrink2 { font-size: 70%; }
SPAN.shrink3 { font-size: 70%; }