TABLE.summary {
border-top: solid 1px #000000;
border-right: solid 1px #000000;
border-left: solid 1px #000000;
border-bottom: solid 1px #000000; 
text-align: center;
}

TD.summary {
border-top: solid 1px #000000;
border-left: solid 1px #000000;
text-align: center;
}
TD.summaryleft {
border-top: solid 1px #000000;
border-left: solid 1px #000000;
text-align: left;
}
TD.summaryright {
border-top: solid 1px #000000;
border-left: solid 1px #000000;
border-right: solid 1px #000000;
text-align: center;
}
TD.summarybottom {
border-top: solid 1px #000000;
border-left: solid 1px #000000;
border-bottom: solid 1px #000000; 
text-align: center;
}

TD.summarybottomleft {
border-top: solid 1px #000000;
border-left: solid 1px #000000;
border-bottom: solid 1px #000000; 
text-align: left;
}

TD.summarybottomright {
border-top: solid 1px #000000;
border-left: solid 1px #000000;
border-right: solid 1px #000000;
border-bottom: solid 1px #000000; 
text-align: center;
}

a:link,
a:visited,
a:active { color: #003399; text-decoration: none }
a:hover  { color: #3366ff; text-decoration: underline }

body,
td { font-family: verdana,arial,helvetica; font-size: 8pt }

input,
select,
textarea { font-family: verdana,arial,helvetica; font-size: 8pt }

.big { font-size: 10pt; line-height: 13pt }
.bigger { font-size: 13pt; line-height: 16pt }
.biggest { font-size: 17pt; line-height: 20pt }

a:link.bluenav,
a:visited.bluenav,
a:active.bluenav { color: #dff9ec }
a:hover.bluenav  { color: #ffffff }

a:link.footer,
a:visited.footer,
a:active.footer { color: #dff9ec }
a:hover.footer  { color: #669999 }

.paragraphs { line-height: 13pt }
.nav { line-height: 13pt }

.red { color: #cc0000 }

.comint-highlight-input {
  /* comint-highlight-input */
  font-weight: bold;
}
.comint-highlight-prompt {
  /* comint-highlight-prompt */
  color: #00008b;
}
.constant {
  /* font-lock-constant-face */
  color: #5f9ea0;
}
.function-name {
  /* font-lock-function-name-face */
  color: #0000ff;
}
.keyword {
  /* font-lock-keyword-face */
  color: #a020f0;
}
.string {
  /* font-lock-string-face */
  color: #bc8f8f;
}
.type {
  /* font-lock-type-face */
  color: #228b22;
}