table.main {
  font-family: helvetica,Arial,sans-serif;
}

a.help {
  vertical-align:super;
  text-decoration: none;
  font-size: 75%;
}

table.command {
  font-family: helvetica,Arial,sans-serif;
  background-color: #eeeeee;
  align: center;
  width: 550px;
  text-align: justify;
}

table {
  text-align: justify;
}

td.blue {
  background-color: lightblue;
}

h2 {
	font-size: 120%;
	padding: 0px;
	border: 0px;
}

table.menu a{
  font-size: 100%;
  text-decoration: none;
  color: black;
}

table.menu a:hover {
  background-color: lightblue;
}

table.menu a.subitem {
  font-size: 80%;
}

p {
  text-align: justify;
}

span.status {
  font-size: 75%;
  font-style: italic;
}

li.paper {
  font-family: helvetica,Arial,sans-serif;
  padding-bottom: 6px;
  font-size: 80%;
}

table.list {
  font-family: helvetica,Arial,sans-serif;
  padding: 0px;
}

table.list td {
	border: 1px dotted;
	padding: 4px;
	margin: 0px;
}

table.list a {
	text-decoration: none;
}

table.list a:hover {
	text-decoration: underline overline;
}

span.name { border-bottom: gray; border-bottom-style: dashed; border-bottom-width: thin; padding-bottom: 0%;}

div.command { background: #eeeeee; width: 550px; border: 1px; padding: 5px; text-align: left; font-size: 75%; margin-top: 0px}

table.arguments { margin: 0px; padding: 0px;}
table.arguments td { vertical-align: top; border-style: dashed; padding: 5px; border-width: thin; }