+++ /dev/null
-@charset "UTF-8";
-
-/* general ******************************************************************/
-
-body {
- background: rgb(255, 255, 255);
- color: rgb(0, 0, 0);
- margin: 2.5%;
-}
-
-a:link, a:visited {
- text-decoration: underline;
-}
-
-a:active, a:hover, a:focus {
- background: rgb(192, 192, 192);
-}
-
-/* blocks *******************************************************************/
-
-.spacer {
- text-align: center;
-}
-
-.head1 {
- margin: 0.5em 0;
- text-align: center;
- font-weight: bold;
- font-size: xx-large;
-}
-
-.head2 {
- margin: 0.5em 0;
- text-align: left;
- font-weight: bold;
- font-size: x-large;
-}
-
-.text {
- margin: 1em 0;
- text-align: left;
-}
-
-/* inline decorations *******************************************************/
-
-.icon32 {
- border: 0;
- width: 32px;
- height: 32px;
-}
-
-.rule {
- border: 0;
- height: 4px;
- width: 100%;
-}
-
-.w3c {
- margin: 0 0.5em;
- border: 0;
- width: 88px;
- height: 32px; /* this should be 31px */
-}
-
-/* terms ********************************************************************/
-
-.separator {
- background: rgb(255, 255, 255);
- color: rgb(0, 0, 0);
-}
-
-.sort {
- background: rgb(255, 255, 255);
- color: rgb(128, 0, 255);
-}
-
-.lref {
- background: rgb(255, 255, 255);
- color: rgb(0, 0, 0);
-}
-
-.gref {
- background: rgb(255, 255, 255);
- color: rgb(0, 0, 255);
-}
-
-.appl {
- background: rgb(255, 255, 255);
- color: rgb(0, 0, 0);
-}
-
-.cast {
- background: rgb(255, 255, 255);
- color: rgb(255, 0, 0);
-}
-
-.local {
- background: rgb(255, 255, 255);
- color: rgb(0, 160, 0);
-}
-
-.global {
- background: rgb(255, 255, 255);
- color: rgb(0, 0, 0);
-}