body {
    padding: 0px 0px;
    margin: 0px 0px; 
    padding-left: 1em;
    background-color: white; 
    font-family: 'Open Sans', sans-serif;
    background-repeat: no-repeat;
    background-size: 100%;     
}

#page {
    display: block;
    padding: 0px;
    margin: 0px;
    padding-bottom: 10px; }

#header { 
    min-height: 100px;
    max-width: 760px;
    margin: 0 auto; 
    padding-left: 80px;
    padding-right: 80px;
    padding-top: 30px;
}

#header h1 {
    padding: 0; 
    margin: 0;
}

/* Menu */
ul#menu { 
    padding: 0;
    display: block;
    margin: auto;
}

ul#menu li, div.button {
    display: inline-block;
    background-color: white;
    padding: 5px;
    font-size: .70em;
    text-transform: uppercase;
    width: 30%;
    text-align: center;
    font-weight: 600;
}

div.button {
	margin-top:5px;
    width: 40%;
}

#button_block {margin-top:50px;}

ul#menu a.hover li  {
    background-color: red;
}

/* Contents */

#main, #main_home {
    display: block;
    padding: 80px;
    padding-top: 60px; /* BCP */
    font-size: 100%;
    line-height: 100%;
    max-width: 760px;
    background-color: #ffffff;
    margin: 0 auto; 
}

#main_home {
    background-color: rgba(255, 255, 255, 0.5);
}

#index_content div.intro p {
    font-size: 12px;
}

#main  h1 {
    /* line-height: 80%; */
    line-height: normal;
    padding-top: 3px;
    padding-bottom: 4px;
    /* Demitri: font-size: 22pt; */
    font-size: 200%; /* BCP */
}

/* allow for multi-line headers */
#main  a.idref:visited {color : #416DFF; text-decoration : none; }
#main  a.idref:link {color : #416DFF; text-decoration : none; }
#main  a.idref:hover {text-decoration : none; }
#main  a.idref:active {text-decoration : none; }

#main  a.modref:visited {color : #416DFF; text-decoration : none; }
#main  a.modref:link {color : #416DFF; text-decoration : none; }
#main  a.modref:hover {text-decoration : none; }
#main  a.modref:active {text-decoration : none; }

#main .keyword { color : #697f2f }
#main { color: black }

/* General section class - applies to all .section IDs */
.section {
    padding-top: 12px; 
    padding-bottom: 11px; 
    padding-left: 8px; 
    margin-top: 5px;
    margin-bottom: 3px;
    margin-top: 18px;
    font-size : 125%;
    color: #ffffff;
}

/* Book title in header */
.booktitleinheader {
    color: #000000;
    text-transform: uppercase;
    margin: 5px auto; 
    font-weight: 300;
    letter-spacing: 1px;
    font-size: 125%;
    margin-left: 0px;
 }

/* Chapter titles */
.libtitle {
    max-width: 860px;
    text-transform: uppercase;
    margin: 5px auto; 
    font-weight: 500;
    padding-bottom: 2px; 
    font-size: 120%;
    letter-spacing: 3px;
 }

.subtitle {
    display: block; 
    padding-top: 10px; 
    font-size: 70%;
    line-height: normal;
}

h2.section {
    color: #2a2c71;
    background-color: transparent;
    padding-left: 0px; 
    padding-top: 0px;  
    padding-bottom: 0px; 
    margin-top: 0px;
    font-size : 135%; }

h3.section {
    /* background-color: rgb(90%,90%,100%); */
    background-color: white; 
    /* padding-left: 8px; */
    padding-left: 0px;
    /* padding-top: 7px;  */
    padding-top: 0px; 
    /* padding-bottom: 0px; */
    padding-bottom: 0.5em; 
    /* margin-top: 9px; */
    margin-top: 4px;
    font-size : 115%;
    color:black;
}
    
h4.section { 
    margin-top: .2em; 
    background-color: white;
    color: #2a2c71;
    padding-left: 0px; 
    padding-top: 0px; 
    padding-bottom: 0.5em; /* 0px;  */
    font-size : 100%;
    font-style : bold;
    text-decoration : underline;
}

#header p {
    font-size: 13px;
}

/* Sets up Main ID and margins */

#main .doc {
    margin: 0px auto;
    font-size: 14px;
    line-height: 22px;
    /* max-width: 570px; */
    color: black;
    /* text-align: justify; */
    border-style: plain;
    padding-top: 18px;
}

.quote { 
    margin-left: auto;
    margin-right: auto;
    width: 40em;
    color: darkred;
} 

.loud {
    color: darkred;
}

pre {
    margin-top: 0px;
    margin-bottom: 0px;
}

.inlinecode { 
    display: inline;
    /* font-size: 125%; */
    color: #444444;
    font-family: monospace } 

.doc .inlinecode { 
    display: inline;
    font-size: 105%;
    color: rgb(35%,35%,70%); 
    font-family: monospace } 

.doc .inlinecode .id { 
/* I am changing this to white in style below:
    color: rgb(35%,35%,70%); 
*/
} 

h1 .inlinecode .id, h1.section span.inlinecode {
	color: #ffffff;
}

.inlinecodenm { 
    display: inline;
    /* font-size: 125%; */
    color: #444444;
}

.doc .inlinecodenm { 
    display: inline;
    color: rgb(35%,35%,70%); 
}

.doc .inlinecodenm .id { 
    color: rgb(35%,35%,70%); 
} 

.doc .code { 
    display: inline; 
    font-size: 110%; 
    color: rgb(35%,35%,70%);
    font-family: monospace;
    padding-left: 0px;
}

.comment { 
    display: inline;
    font-family: monospace;
    color: rgb(50%,50%,80%); 
} 

.inlineref { 
    display: inline;
    /* font-family: monospace; */
    color: rgb(50%,50%,80%); 
} 

.show::before {
    /* content: "more"; */
    content: "+";
}

.show { 
    background-color: rgb(93%,93%,93%);
    display: inline;
    font-family: monospace;
    font-size: 60%; 
    padding-top: 1px; 
    padding-bottom: 2px; 
    padding-left: 4px;
    padding-right: 4px;
    color: rgb(60%,60%,60%); 
} 

/*
.show { 
    display: inline;
    font-family: monospace;
    font-size: 60%; 
    padding-top: 0px; 
    padding-bottom: 0px; 
    padding-left: 10px;
    border: 1px;
    border-style: solid;
    color: rgb(75%,75%,85%); 
} 
*/

.proofbox {
    font-size: 90%;
    color: rgb(75%,75%,75%); 
}

#main .less-space {
    margin-top: -12px;
}

/* Inline quizzes */
.quiz:before { 
    color: rgb(40%,40%,40%);
    /* content: "- Quick Check -" ; */
    display: block;
    text-align: center;
    margin-bottom: 5px;
}
.quiz { 
    border: 4px;
    border-color: rgb(80%,80%,80%);
    /*
    margin-left: 40px;
    margin-right: 100px;
   */
    padding: 5px;
    padding-left: 8px;
    padding-right: 8px;
    margin-top: 10px;
    margin-bottom: 15px;
    border-style: solid;
}

/* For textual ones... */
.show-old { 
    display: inline;
    font-family: monospace;
    font-size: 80%; 
    padding-top: 0px; 
    padding-bottom: 0px; 
    padding-left: 3px;
    padding-right: 3px;
    border: 1px;
    margin-top: 5px;   /* doesn't work?! */
    border-style: solid;
    color: rgb(75%,75%,85%); 
} 

.largebr { 
    margin-top: 10px;
} 

.code { 
    padding-left: 20px;
    font-size: 14px;
    font-family: monospace;
    line-height: 17px;
} 

/* Working:
.code { 
    display: block;
    padding-left: 0px; 
    font-size: 110%;
    font-family: monospace;
 } 
*/

.code-space {
    max-width: 50em;
    margin-top: 0em;
    /* margin-bottom: -.5em; */
    margin-left: auto;
    margin-right: auto;
}

.code-tight {
    max-width: 50em;
    margin-top: .6em;
    /* margin-bottom: -.7em; */
    margin-left: auto;
    margin-right: auto;
}

hr.doublespaceincode {
    height: 1pt;
    visibility: hidden;
    font-size: 10px;                   
}

/*
code.br {
  height: 5em;
}
*/

#main .citation {
    color: rgb(70%,0%,0%); 
    text-decoration: underline;
}

table.infrule {
    border: 0px;
    margin-left: 50px;
    margin-top: .5em;
    margin-bottom: 1.2em;
}

td.infrule {
    font-family: monospace;
    text-align: center;
    /*    color: rgb(35%,35%,70%);  */
    padding: 0px;
    line-height: 100%;
}

tr.infrulemiddle hr {
    margin: 1px 0 1px 0;
}

.infrulenamecol {
    color: rgb(60%,60%,60%); 
    font-size: 80%;
    padding-left: 1em;
    padding-bottom: 0.1em
}

#footer {
    font-size: 65%;
    font-family: sans-serif; 
}

.id { display: inline; }

.id[type="constructor"] { 
    color: #697f2f;
}

.id[type="var"] { 
    color: rgb(40%,0%,40%);
}

.id[type="variable"] { 
    color: rgb(40%,0%,40%);
}

.id[type="definition"] { 
    color: rgb(0%,40%,0%);
}

.id[type="abbreviation"] { 
    color: rgb(0%,40%,0%);
}

.id[type="lemma"] { 
    color: rgb(0%,40%,0%);
}

.id[type="instance"] { 
    color: rgb(0%,40%,0%);
}

.id[type="projection"] { 
    color: rgb(0%,40%,0%);
}

.id[type="method"] { 
    color: rgb(0%,40%,0%);
}

.id[type="inductive"] { 
    color: #034764;
}

.id[type="record"] { 
    color: rgb(0%,0%,80%);
}

.id[type="class"] { 
    color: rgb(0%,0%,80%);
}

.id[type="keyword"] { 
    color : #697f2f;
    /*     color: black; */
}

.inlinecode .id { 
    color: rgb(0%,0%,0%);
}

.nowrap {
    white-space: nowrap;
}

/* TOC */

#toc h2 {
/*    padding-top: 13px; */
    padding-bottom: 13px; 
    padding-left: 8px; 
    margin-top: 5px;
    margin-top: 20px;
    /* OLD: padding: 10px;
       line-height: 120%;
       background-color: rgb(60%,60%,100%); */
}

#toc h2 .select { background-image: url('media/image/arrow_down.jpg'); }
div#sec1.hide { display: none; }

#toc ul {
    padding-top: 8px;
    margin-bottom: -8px;
    font-size: 14px;
    padding-left: 0;
}

#toc li {
    font-weight: 600;
    list-style-type: none;
    padding-top: 12px;
    padding-bottom: 8px;
}

#toc li li {
    font-weight: 300;
    list-style-type: circle; 
    padding-bottom: 3px;
    padding-top: 0px;
    margin-left: 19px;
}




/*  Accordion Overrides  */

/*  Widget Bar  */
.ui-state-default,
.ui-widget-content .ui-state-default,
.ui-widget-header .ui-state-default,
.ui-button,
/* We use html here because we need a greater specificity to make sure disabled
   works properly when clicked or hovered */
html .ui-button.ui-state-disabled:hover,
html .ui-button.ui-state-disabled:active {
    border: none!important;
    /* BCP 3/17: I like it better without the rules...
       border-bottom: 1px solid silver!important; */
    background: white !important; 
    font-weight: normal;
    color: #454545!important;
    font-weight: 400!important;
    margin-top: 0px!important;
    
}

/* Misc visuals
----------------------------------*/

/* Corner radius */
.ui-corner-all,
.ui-corner-top,
.ui-corner-left,
.ui-corner-tl {
 border-top-left-radius: 0px!important; 
}

.ui-corner-all,
.ui-corner-top,
.ui-corner-right,
.ui-corner-tr {
 border-top-right-radius: 0px!important;
}

.ui-corner-all,
.ui-corner-bottom,
.ui-corner-left,
.ui-corner-bl {
 border-bottom-left-radius: 0px!important;
}

.ui-corner-all,
.ui-corner-bottom,
.ui-corner-right,
.ui-corner-br {
    border-bottom-right-radius: 0px!important;
}

html .ui-button.ui-state-disabled:focus {
	color: red!important;
}

/*  Remove Icon  */
.ui-icon { display: none!important; }

/*  Widget  */
.ui-widget-content {
	border: 1px solid #9e9e9e;
	border-bottom-color: #b2b2b2;
}

.ui-state-active {
    background: silver !important;
}

.ui-widget-content {
    border: none!important;
    background: #ffffff;
    color: #333333;
    border-bottom: 1px solid #b2b2b2!important;
}

.ui-accordion .ui-accordion-content {
	padding: 0 2.2em 2em .75em !important;
	border-top: 0;
    overflow: auto;
}


/* Index */

#index {
    margin: 0;
    padding: 0;
    width: 100%;
    font-style : normal;
}

#index #frontispiece {
    margin: auto;
    padding: 1em;
    width: 700px;
}

.booktitle {
    font-size : 300%; line-height: 100%; font-style:bold;
    color: white;
    padding-top: 70px;
    padding-bottom: 20px; }
.authors { font-size : 200%;
           line-height: 115%;  }
.moreauthors { font-size : 170%  }
.buttons { font-size : 170%;
           margin-left: auto;
           margin-right: auto;
           font-style : bold;
         }

A:link {text-decoration: none; color:black}
A:visited {text-decoration: none; color:black}
A:active {text-decoration: none; color:black}
A:hover {text-decoration: none; color: #555555 }

#index #entrance {
    text-align: center;
}

/* This was removed via CSS but the HTML is still generated */
#index #footer {
    display: none;
}

.paragraph {
    height: 0.6em;
}

ul.doclist {
    margin-top: 0em;
    margin-bottom: 0em;
}

/* Index styles */

/* Styles the author box (Intro class) and With (column class) */

.column {
    float:left;
    width: 43%;
    margin:0 10px;
    text-align: left;
    font-size: 15px;
    line-height: 25px;
    padding-right: 20px;
    min-height: 340px;
}

.smallauthors {
    font-size: 19px;
    line-height: 25px;
}

.mediumauthors {
    font-size: 23px;
    line-height: 33px;
}

.largeauthors {
    font-size: 28px;
    line-height: 40px;
}

.intro {
    width: 35%; 
    font-size: 21px;
    line-height: 27px;
    font-weight: 600;
    padding-right: 20px;
}

.column.pub {
    width: 40%;
    margin-bottom: 20px;
}

#index_content {
    width: 100%!important;
    display: block;
    min-height: 400px;
}

div.column.pub table tbody tr td {
    text-align: center; padding: 10px;
}
div.column.pub table tbody tr td p {
    text-align: left; 	
    margin-top: 0;
    font-weight: 600;
    font-size: 13px!important;
    line-height: 18px;
}

/* Tables */

td.tab {
    height: 16px;
    font-weight: 600; 
    padding-left: 5px; 
    text-align: left!important;
}

/* Styles tables on the index -- body class sf_home is used there */

body.sf_home table {
    min-height: 450px;
    vertical-align: top;
}

body.sf_home table td {
    vertical-align: top;
    
}	
body.sf_home table td p {
    min-height: 100px;
    
}

table.logical { 
    background-color: rgba(144, 160, 209, 0.5);  }
    
    
table.logical tbody tr td.tab { background-color: #91a1d1; }
table.language_found { background-color: rgba(178, 88, 88, 0.5);  }
table.language_found  tbody tr td.tab { background-color: #b25959; }

table.algo {  background-color: rgba(194, 194, 108, 0.5); }
table.algo  tbody tr td.tab { background-color: #c2c26c; }

table.qc {  background-color: rgba(185, 170, 185, 0.5); }
table.qc tbody tr td.tab { background-color: #8b7d95; }

/* Suggested background color for next volume */
#     #c07d62

.ui-draggable, .ui-droppable {
    background-position: top;
}

/* Google Fonts - Local Use Styles */

@font-face {
    font-family: 'Open Sans';
    font-weight: 300;
    font-style: normal;
    src: url('../media/font/Open-Sans-300/Open-Sans-300.eot');
    src: url('../media/font/Open-Sans-300/Open-Sans-300.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Light'),
    local('Open-Sans-300'),
    url('../media/font/Open-Sans-300/Open-Sans-300.woff2') format('woff2'),
    url('../media/font/Open-Sans-300/Open-Sans-300.woff') format('woff'),
    url('../media/font/Open-Sans-300/Open-Sans-300.ttf') format('truetype'),
    url('../media/font/Open-Sans-300/Open-Sans-300.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 400;
    font-style: normal;
    src: url('../media/font/Open-Sans-regular/Open-Sans-regular.eot');
    src: url('../media/font/Open-Sans-regular/Open-Sans-regular.eot?#iefix') format('embedded-opentype'),
    local('Open Sans'),
    local('Open-Sans-regular'),
    url('../media/font/Open-Sans-regular/Open-Sans-regular.woff2') format('woff2'),
    url('../media/font/Open-Sans-regular/Open-Sans-regular.woff') format('woff'),
    url('../media/font/Open-Sans-regular/Open-Sans-regular.ttf') format('truetype'),
    url('../media/font/Open-Sans-regular/Open-Sans-regular.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 600;
    font-style: normal;
    src: url('../media/font/Open-Sans-600/Open-Sans-600.eot');
    src: url('../media/font/Open-Sans-600/Open-Sans-600.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Semibold'),
    local('Open-Sans-600'),
    url('../media/font/Open-Sans-600/Open-Sans-600.woff2') format('woff2'),
    url('../media/font/Open-Sans-600/Open-Sans-600.woff') format('woff'),
    url('../media/font/Open-Sans-600/Open-Sans-600.ttf') format('truetype'),
    url('../media/font/Open-Sans-600/Open-Sans-600.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 700;
    font-style: normal;
    src: url('../media/font/Open-Sans-700/Open-Sans-700.eot');
    src: url('../media/font/Open-Sans-700/Open-Sans-700.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Bold'),
    local('Open-Sans-700'),
    url('../media/font/Open-Sans-700/Open-Sans-700.woff2') format('woff2'),
    url('../media/font/Open-Sans-700/Open-Sans-700.woff') format('woff'),
    url('../media/font/Open-Sans-700/Open-Sans-700.ttf') format('truetype'),
    url('../media/font/Open-Sans-700/Open-Sans-700.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 800;
    font-style: normal;
    src: url('../media/font/Open-Sans-800/Open-Sans-800.eot');
    src: url('../media/font/Open-Sans-800/Open-Sans-800.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Extrabold'),
    local('Open-Sans-800'),
    url('../media/font/Open-Sans-800/Open-Sans-800.woff2') format('woff2'),
    url('../media/font/Open-Sans-800/Open-Sans-800.woff') format('woff'),
    url('../media/font/Open-Sans-800/Open-Sans-800.ttf') format('truetype'),
    url('../media/font/Open-Sans-800/Open-Sans-800.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 300;
    font-style: italic;
    src: url('../media/font/Open-Sans-300italic/Open-Sans-300italic.eot');
    src: url('../media/font/Open-Sans-300italic/Open-Sans-300italic.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Light Italic'),
    local('Open-Sans-300italic'),
    url('../media/font/Open-Sans-300italic/Open-Sans-300italic.woff2') format('woff2'),
    url('../media/font/Open-Sans-300italic/Open-Sans-300italic.woff') format('woff'),
    url('../media/font/Open-Sans-300italic/Open-Sans-300italic.ttf') format('truetype'),
    url('../media/font/Open-Sans-300italic/Open-Sans-300italic.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 400;
    font-style: italic;
    src: url('../media/font/Open-Sans-italic/Open-Sans-italic.eot');
    src: url('../media/font/Open-Sans-italic/Open-Sans-italic.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Italic'),
    local('Open-Sans-italic'),
    url('../media/font/Open-Sans-italic/Open-Sans-italic.woff2') format('woff2'),
    url('../media/font/Open-Sans-italic/Open-Sans-italic.woff') format('woff'),
    url('../media/font/Open-Sans-italic/Open-Sans-italic.ttf') format('truetype'),
    url('../media/font/Open-Sans-italic/Open-Sans-italic.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 600;
    font-style: italic;
    src: url('../media/font/Open-Sans-600italic/Open-Sans-600italic.eot');
    src: url('../media/font/Open-Sans-600italic/Open-Sans-600italic.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Semibold Italic'),
    local('Open-Sans-600italic'),
    url('../media/font/Open-Sans-600italic/Open-Sans-600italic.woff2') format('woff2'),
    url('../media/font/Open-Sans-600italic/Open-Sans-600italic.woff') format('woff'),
    url('../media/font/Open-Sans-600italic/Open-Sans-600italic.ttf') format('truetype'),
    url('../media/font/Open-Sans-600italic/Open-Sans-600italic.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 700;
    font-style: italic;
    src: url('../media/font/Open-Sans-700italic/Open-Sans-700italic.eot');
    src: url('../media/font/Open-Sans-700italic/Open-Sans-700italic.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Bold Italic'),
    local('Open-Sans-700italic'),
    url('../media/font/Open-Sans-700italic/Open-Sans-700italic.woff2') format('woff2'),
    url('../media/font/Open-Sans-700italic/Open-Sans-700italic.woff') format('woff'),
    url('../media/font/Open-Sans-700italic/Open-Sans-700italic.ttf') format('truetype'),
    url('../media/font/Open-Sans-700italic/Open-Sans-700italic.svg#OpenSans') format('svg');
}

@font-face {
    font-family: 'Open Sans';
    font-weight: 800;
    font-style: italic;
    src: url('../media/font/Open-Sans-800italic/Open-Sans-800italic.eot');
    src: url('../media/font/Open-Sans-800italic/Open-Sans-800italic.eot?#iefix') format('embedded-opentype'),
    local('Open Sans Extrabold Italic'),
    local('Open-Sans-800italic'),
    url('../media/font/Open-Sans-800italic/Open-Sans-800italic.woff2') format('woff2'),
    url('../media/font/Open-Sans-800italic/Open-Sans-800italic.woff') format('woff'),
    url('../media/font/Open-Sans-800italic/Open-Sans-800italic.ttf') format('truetype'),
    url('../media/font/Open-Sans-800italic/Open-Sans-800italic.svg#OpenSans') format('svg');
}

/* A few specific things for the top-level SF landing page */

body.sf_home {background-color: #ededed; background-image: url(../media/image/core_mem_bg.jpg); }       

body.sf_home #header {
    background-image: url(../media/image/core_mem_hdr_bg.jpg);  
    padding-bottom: 20px;
}

body.sf_home #main_home {
    background-color: transparent;
}