body {
  font-family:     Arial, Helvetica, sans-serif;
  background-color: #ffffff
}

a {text-decoration: none}
a:link { color: #2020a8 }
a:visited { color: #2020a8 }

h1 {
  font-family: sans-serif;
  font-size: 2em;
  text-align: left;
}

h2 {
  font-family: sans-serif;
  font-size: 1.5em;
  text-align: left;
}

.left { text-align: left }
.right { text-align: right }
.center { text-align: center }
.float_left { float: left;  padding-right: 3em; }
.float_right { float: right;  padding-left: 3em; }
.clear_float { clear: both }
.clear_left { clear: left }
.clear_right { clear: right }

.smaller { font-size: small }
.polymake_green { background-color: #77ec9e }

span.math { white-space: nowrap; font-style: italic }
span.math sup, span.math sub { font-style: normal }

a.note:link, a.note:visited, a.hlarg { color: #08c008; }
a.hlarg { font-style: italic }

div.note { position: absolute; z-index: 2; visibility: hidden; max-width: 70%; background: inherit;
	   border: 2px solid #000099; padding: 0.5em; }

.quote { white-space: pre; }

span.code { font-family: monospace; white-space: nowrap; }
span.sans { font-family: sans-serif; white-space: nowrap; }
span.nowrap { white-space: nowrap; }
div.code, div.code_cont { font-family: monospace; white-space: pre; }

div.topic { white-space: nowrap; }
div.subtopic { white-space: nowrap; margin-left: 1em; }
div.descr, table.descr { margin-left: 2em; }
div.descr>div.descr, div.descr>table.descr { margin-left: 0em; }
ol.descr, ul.descr, blockquote.descr { padding-left: 0em; margin-left: 3.5em; }

*.code + *.descr, *.topic + *.descr, *.subtopic + *.descr, *.descr + *.code_cont, *.code_cont + *.descr { margin-top: 0.5em }
*.descr + *.code, *.descr + *.topic, *.code_cont + *.code, *.code_cont + *.topic { margin-top: 1em }
*.descr + *.subtopic { margin-top: 0.75em }
*.descr + *.descr { margin-top: 0.25em }
*.topic + *.topic { margin-top: 0px }
*.descr { padding-top: 0px; padding-bottom: 0px; margin-bottom: 0px; }

*.class_body { border-left: 3px double gray; border-bottom: 3px double gray;
	       padding-left: 1em; padding-bottom: 1em; margin-top: 1em; margin-bottom: 2em }

ul>li, ol>li { margin-top: 1em }
li>ul>li, li>ol>li { margin-top: 0.7em }
li>ul + div, li>ol + div { margin-top: 0.7em }
ul.compact>li, ol.compact>li { margin-left: -1em; margin-top: 0px; }

ul.descr>li, ol.descr>li, li>div + div { margin-top: 0.5em; }
ul.compact>li>div + div, ol.compact>li>div + div { margin-top: 0em }

table.borderless { border-style: none; border-spacing: 2em 1em; }
table.borderless_compact { border-style: none; border-spacing: 1em 0em; }

caption { text-decoration: underline; }