body 
  { 
  ; border: 1px solid black
  ; margin-left: 20px
  ; margin-right: 20px
  ; margin-top: 10px
  ; margin-bottom: 10px
  ; padding: 10px
  }

pre.orig
  { border: none
  ; background: none
  }

pre
  { border: dashed 1px black
  ; background: #80d0f0
  ; margin: 5px
  ; margin-left: 25px
  ; padding: 5px
}

h1 {
   ; text-align: center
   ; border-bottom: solid 1px black
   }

h2 {
   ; border-bottom: solid 5px #4040a0
   ; margin-right: 10px
   ; text-align: left
   ; padding-top: 10px
   }

h3 {
   ; width: 50%
   ; border-bottom: dotted 2px #4040a0
   }

p {
  ; text-align: justify
  }

span.u {
    ; background: orange
    ; border: solid 1px black
    ; padding: 2px
    }

img.pic {
	; float: right
	; margin: 5px
	; margin-left: 20px
	; margin-right: 10px
	; margin-top: -10px
	; margin-bottom: -30px
	; padding-left: 10px
	}

div.links 
	  { float: left
	  ; width: 300px
	  ; border: solid 1px black
	  ; border-right: solid 1px black
	  ; border-bottom: solid 1px black
	  ; background: white
	  ; font-variant: small-caps
	  ; padding-right: 0px
	  ; padding-bottom: 0px
	  ; margin-right: 20px
	  }

.links table 
       { border-collapse: collapse  ; border: solid 1px white
       ; background: #e0e0ff
       ; width: 100%
       }

.links td        { border: solid 1px white }
.links td:hover  { background: yellow }
.links th        { border: solid 1px white }

.links a:hover   { width: 100% }
.links a:hover   { color: black ; text-decoration: none }
.links a:link    { color: black ; text-decoration: none }
.links a:visited { color: black ; text-decoration: none }
.links a:active  { color: black ; text-decoration: none }