div.body	{ color: #333333; 
		  max-width: 800px;
		  padding-left: 10px;
		  font-size: smaller; 
		  font-family: Verdana, Tahoma, Arial, sans-serif; }
span.sec-head	{ font-weight: bold; color: blue; } 
span.ssec-head	{ font-weight: bold; color: blue; }
span.addr	{ text-decoration: underline; }
span.arg	{ font-style: italic; }
span.config	{ font-weight: bold; }
span.diag	{ font-weight: bold; }
span.emph	{ font-style: italic; }
span.farg	{ font-style: underline; }
span.file	{ font-style: italic; }
span.flag	{ font-weight: bold; }
span.name	{ font-weight: bold; } 
span.type	{ font-weight: italic; }
span.utility	{ font-weight: bold; }
table.header	{ border-bottom: 1px dotted #cccccc; }
table.footer	{ border-top: 1px dotted #cccccc; }