.figure { text-align: center;
          margin-top: 10px;}

.figure table .numbers { text-align: right; }

.figure table { margin: auto;
                border-style: none ; }

.figure th, td { padding: 0px; 
                 border-style: none ;}

.figure table th, td  pre { padding: 0px; }

.figure  table .example { border: 1px solid ; } 

.figure table  .caption { text-align: center; }





.algo { text-align: center;
        margin-top: 10px; }

.algo table { margin: auto; 
              border-style: none ;
	      border-collapse: collapse ; }


.algo table tr { height: 1.2em; 
                 border-style: none; }

.algo table td { font-family: monospace; 
                 padding-left: 5px;
                 padding-right: 5px; }

.algo table .line { 
                    border-left: 1px solid;
                    border-right: 1px solid;}



.algo table .line-bottom { border-bottom: 1px solid;
                           border-left: 1px solid;
                           border-right: 1px solid; }

.algo table .line-top { border-top: 1px solid;
                        border-left: 1px solid;
                        border-right: 1px solid; }

.algo table .numbers { text-align: right;
                       border-style: none; }
                  
.smaller {  font-size: smaller }
.huge { font-size: xx-large }
.large { font-size: x-large }
.big10 { font-size: 1000% }
.big5 { font-size: 500% }
sub {font-size: smaller }
td pre {  margin: 0.5em; font-size: smaller }
td hr {  margin: 0.5em }

pre.rewritten	{ border: thin solid #88AA88;
                  background-color: #E8F0E8;
                  margin: 1em 4em 1em 0em ; }