/* CSS Stylesheet for XML Common Logic (XCL) 1.0 Specification
   $Id: xcl.css,v 1.5 2005/12/16 10:47:36 altheim Exp $
 */
/* <style type="text/css"> */
  body {
    background-color: white ;
    background: url("img/background.png") left top repeat-y scroll ;
    margin-top:    1em ;
    margin-left:   12% ;
    margin-right:  12% ;
    margin-bottom: 50em ;
  }
  table.pgheader {
    margin-left :  1% ;
    margin-right : 2% ;
    width : 100% ;
  }
 /* small light purple links following certain block elements. */
 .plink, .plinks {
    font-family : "Helvetica", sans-serif ; 
    font-size : x-small ;
    font-style : normal ;
    font-weight : normal ;
    text-decoration : none ;
    color : #cabee0 ;
 /* color : #C8A8FF ; */
  }
/* a:link     { color : #663399 } */
  .header {
    margin-top:  -8px ;
    margin-left: -8px ;
  }
  div.abstract { 
    padding-top : 1em ;
  }
  p.abstract { 
    margin-right : 25% ;
    font-family : "Times New Roman", "Times", serif ;
    font-size : small ; 
    font-style : plain ; 
    color : #500080 ; 
  }
  h1,h2,h3,h4 {
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    padding-top : 0.5em ;
    margin-left : 0em ;
  }
  h1 {
    font-size : xx-large ;
    color : #400070 ;
 /* color : red ; */
  }
  h1.div0 { /* neutral heading */
    font-size : xx-large ;
    color : #603090 ;
 /* color : red ; */
  }
  h2 {
    padding-top : 2em ;
    padding-bottom : 0.5em ;
    font-size : x-large ;
    color : #400070 ; 
 /* color : orange ; */
  }
  h3 {
    font-size : large ;
    color : #400070 ; 
 /* color : yellow ; */
  }
  h4 {
    font-size : medium ;
    font-style : italic ;
    color : #500080 ;
 /* color : #008000 ; */
  }
  h5,h6 {
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : medium ;
    font-style : italic ;
  }
  h5.diff {
    color : #698900 ;
  }
  h6 {
    color : #7000A0 ;
  }
  div {
    margin-left: 2em ;
  }
  .sect  {
    margin-left :  1em ;
    margin-right : 1em ;
  }
  .sect1 {
    margin-left : 1em ;
    margin-right : 1em ;
  }
  .sect2 {
    margin-left : 1em ;
    margin-right : 1em ;
  }
  .sect3 {
    margin-left : 1em ;
    margin-right : 1em ;
  }
  .hdt {
    font-family : "Times New Roman", "Times", serif ;
    font-size : small ;
    font-weight : bold ;
    color : #5000B0 ;
    padding-right : 0em ;
  }
  blockquote {
    font-family : "Verdana", "Lucida", "Helvetica", sans-serif ;
    margin-right : 25% ;
    margin-left :  3em ;
    padding-top : 1em ;
    padding-bottom : 2em ;
    font-size : 80% ;
    font-style : italic ;
    color : #3000B0 ;
  }
  .linkimg { 
    align : right ;
    border-style : none ; 
  }
  .doctitle { 
    padding-top : 0.5em ;
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : xx-large ;
    color : #500080 ; 
  }
  .subtitle { 
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : x-large ; 
    padding-bottom : 0.5em ;
    color : #500080 ; 
  }
  .author { 
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : medium ; 
    font-style : italic ; 
    color : #500080 ; 
  }
  .footer { 
    margin-left : 0em ;
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : 75% ;
    text-align : left ;
  }
  .footnote { 
    margin-left : -1em ;
    font-size : small ;
    text-align : left ;
    text-indent : -1em ;
  }
  .ref {
    font-family : "Times New Roman", "Times", serif ;
    font-size : medium ;
    font-weight : bold ;
  }
  .xref {
    font-family : "Times New Roman", "Times", serif ;
    font-size : medium ;
    text-decoration : none ;
  }
  pre {
    font-family : "Courier New", "Courier", monospace ;
    white-space : pre ;
    color : #100050 ;
    font-size : medium ;
    margin-left : 2em ;
  }
  pre.markup {
    font-size : medium ;
    background-color : #ddddff ;
    padding-top : 0.5em ;
    padding-bottom : 0.5em ;
    font-size : 80% ;
    color : #100050 ;
  }
  .uhl { /* un-hilight */
    color : #817c9b ;
  }
  div.toc {
    padding-bottom : 1em ;
  }
  p.nav {
    margin-left : -2em ;
    margin-bottom: 4em ;
    font-family : "Courier New", "Courier", monospace ;
    font-size : small ;
    color : #300070 ;
  }
  .center { 
    text-align : center 
  }
  .mailto { text-decoration : none }
  p.legal {
    font-family : "Times New Roman", "Times", serif ;
    font-size : small ;
    color : #333333  ;
  }
  .note {
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : small ;
    clear : left ;
    margin-left : -7em ;
    margin-right : 25% ;
    color : #2e5a66 ;
  }
  .ednote {
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : small ;
    clear : left ;
    margin-left : -7em ;
    margin-right : 25% ;
    color : #4d747F ;
  }
  ul.none {
    list-style-type : none ; 
  }
  .term { 
    font-weight : bold ;
  }
  .unfinished { /* used in undefined definitions */
    color : #b584a2 ;
  }
  .thead {  /* table headings */
    background-color : #8fbab9 ;
    text-align : left ;
  }
  .even {  /* used in alternate table rows */
    background-color : #daeaea ;
  }
  .odd {  /* used in alternate table rows */
    background-color : #ffffff ;
  }

  table.b {
    border-width : thin ;
    border-color : #5c47b7 ;
  }
  th.b {
    background-color : #5c47b7 ;
    color : white ;
    text-align : left ;
    font-style : italic ;
    vertical-align : top ;
  }
  td.b {
    text-align : left ;
    vertical-align : top ;
  }
  pre.samp {
    font-family : monospace ;
    color : #5010B0 ;
  }
  pre tt {
    font-family : monospace ;
    font-size : medium ;
    color : #b3ce77 ;
  }
  pre.logic {
    font-family : sans-serif ;
    font-size : 120% ;
    color : #100050 ;
  }
  pre.kif {
    font-family : monospace ;
    font-size : 120% ;
    color : #100050 ; ;
  }
  code {
    color : #5010B0 ;
  }
  code {
    color : #400080 ;
  }
  table.elts {
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    margin-left : 0em ;
  }
  table.elts th {
    font-weight: bold;
    background-color : #eafcfd ;
    text-align : left ;
    vertical-align : top ;
    border-top: 1px solid #dbf4f9 ;
    border-left: 1px solid #bee5ed ;
    border-right: 1px solid #c6cccc ;
    border-bottom: 1px solid #c6cccc ;
  }
  table.elts th.elth {
    background-color:  #d4eef4 ;
  }
  table.elts td {
    font-weight: normal;
    background-color : #ffffff ;
    text-align : left ;
    vertical-align : top ;
    border-top:    0px solid #dbf4f9 ;
    border-left:   0px solid #bee5ed ;
    border-right:  1px solid #c6cccc ;
    border-bottom: 1px solid #c6cccc ;
  }
  div.elts {
    margin-left : 2em ;
  }
  div.elts p {
    margin-left : 5em ;
    font-style : italic ;
    font-size : smaller ;
  }
  .prlink {
    text-decoration : none ;
    color : #6f00aa ;
  }
  dl.princ dt {
    padding-top : 0.5em ;
    margin-right : 4em ;
    margin-left : 2em ;
    font-family : "Verdana", "Lucida Sans", "Lucidux Sans", "Lucida", "Helvetica", sans-serif ;
    font-size : medium ;
    font-weight : bold ;
    font-style : italic ;
    color : #6f00aa ;
  }
  dl.princ dd {
    padding-bottom : 0.5em ;
    margin-right : 4em ;
  }
  .tabledisplay {
    padding-top : 1em ;
    padding-bottom : 2em ;
  }
  .neutral {
    margin-left : -4em ;
  }
  .ignore {
    color : #aaaaaa ;
  }
  .ceryle {
    color : #007c87 ;
  }
  .rfc2119 {
    font-style : italic ;
    font-weight : bold ;
  }
  pre.log {
    margin-left : -4em ;
    font-size : small ;
    color : gray ;
  }

/* small light purple links following certain block elements. */
.plink, .plinks {
/* display : none ; */
   font-family : "Helvetica", sans-serif ; 
   font-size : x-small ;
   font-style : normal ;
   font-weight : normal ;
   text-decoration : none ;
   color : #C8A8FF ;
/* color : #8700FF ; */
 }