body {
	background-color: lightblue;
	color: black;
	font-family: arial, geneva, helvetica, sans-serif;
	font-size: 95%;
	margin: 0 auto;
}
a.menu:link {
	color: white;
	text-decoration: none;
}
a.menu:visited {
	color: white;
	text-decoration: none;
}
a.menu:hover {
	color: yellow;
	text-decoration: underline;
}
a.menu:active {
	color: yellow;
	text-decoration: underline;
}
div.top{background-color:black;color: white;border: 1px solid black; padding: 2px 5px;}
a.pjmenu{font-weight: bold;}
a.topmenu{display: block; padding: 0px 10px; text-align: right}
ul.menu {
	list-style-type: none;
	margin: 0;
	padding: 0;
	overflow: hidden;
}
li.menu {
	float: left;
}
.left{
	float: left;
}
.right {
	float: right;
	text-align: center;
}
li {
	margin-bottom: 0.5em;
}
h2 {
	font-weight: bold;
	font-size: 130%;
}
h3 {
	font-weight: bold;
	font-size: 110%;
}
h4 {
	font-weight: bold; 
	font-size: 100%;
}
pre {
	line-height: 100%;
}
div.full-width {
	width: 100%;
}
div.content {
	background-color: white;
	border: 1pt solid navy;
	padding: 20px;
	line-height: 150%;
	text-align: left;
}
div.previous {
	float: left;
	width: 48%;
}
div.next {
	float: right;
	text-align: right;
	width: 48%;
}
div.section-content {
	padding-right: 1em;
	padding-left: 1em
}
div.example-content {
	padding-right: 2em;
	padding-left: 2em;
	line-height: 100%;
}
div.code {
	background-color: #eeeeee;
	width: 100%; 
	line-height: 100%;
	padding: 5px;
	overflow: auto;
}
span.manual {
}
span.input {
	font-weight: bold;
}
span.output {
	color: navy;
}
span.comment {
}
div.footer {
	width: 100%;
	text-align: center;
	font-size: 95%;
}
img {
	border: 1px solid #000000;
}
table, th, td {
	border: 1px solid black;
	border-collapse: collapse;
	text-align: center;
}