body {
	font-family: Helvetica, Arial, sans-serif;
}

h1.title {
	margin-top: 0.10em;
}

h2.directory {
	margin-top: 0.25em;
	margin-bottom: 0;
	font-size: 100%;
}

.classdoc
{
	margin-left: 0.5em;
	margin-right: 0.5em;
	margin-bottom: 0.5em;
	border: 1px solid gray;
	background-color: #ddd;
	padding: 0.5em;
}

.head
{
	background-color: #ffddff;
	font-size: large;
	border-bottom: 1px solid black;
	margin-top: 0;
	margin-bottom: 0;
	padding: 0.25em;
}

.smallHead
{
	background-color: #ffddff;
	font-size: small;
	border-bottom: 1px solid black;
	margin-top: 0;
	margin-bottom: 0;
	padding: 0.25em;
}

.section
{
	border: 1px solid black;
	padding: 0;
	padding-bottom: 0.25em;
	margin-bottom: 0.5em;
}

div.list {
	padding: 0.5em;
}

dt {
	margin-top: 1em;
	margin-bottom: 0;
	padding: 0 0.25em;
	font-family: monospace;
}

dd {
	margin-top: 0.25em;
}