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: 22%;
    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: rgba(255, 255, 255, 0.7);
    margin: 0 auto;
}

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

#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: #000000;
}

/* Book title in header */

.booktitleinheader {
    color: #000000;
    text-transform: uppercase;
    font-weight: 300;
    letter-spacing: 1px;
    font-size: 125%;
    margin-left: 0px;
    margin-bottom: 22px;
}

/* 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; */
    margin-top: 9px;
    /* BCP 2/20 */
    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;  (BCP 2/20) */
    margin-top: 9px;
    /* BCP 2/20 */
    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;
    /* This might work better after changing back to standard coqdoc: */
    padding-top: 10px;
    /* 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;
    color: #444444;
    font-family: JetbrainsMono;
    font-weight: bold;
    /* background-color: rgb(235, 235, 235); */
    /* border-radius: .4rem; */
    padding: .1rem 0.2rem;
}

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

.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: #444444;
}

.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: JetbrainsMono;
    padding-left: 0px;
}

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

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

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

.show {
    background-color: rgb(93%, 93%, 93%);
    display: inline;
    font-family: JetbrainsMono;
    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: JetbrainsMono;
    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: JetbrainsMono;
    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: JetbrainsMono;
    line-height: 17px;
}

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

.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: JetbrainsMono;
    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[title="constructor"] {
    color: #697f2f;
}

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

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

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

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

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

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

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

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

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

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

.id[title="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.ui-accordion-header {
    padding: .5em .5em .5em .7em;
    outline: none;
}

#toc .ui-accordion .ui-accordion-content {
    padding: 0.5em 2.5em 0.8em .9em;
    border-top: 0;
    margin-bottom: 1em;
    /* bottom rule */
    border: none;
    border-bottom: 1px solid transparent;
    transition: border-bottom-color 0.25s ease-in;
    transition-delay: 0.15s;
}

#toc .ui-accordion .ui-accordion-content-active {
    border-bottom: 1px solid #9b9b9b;
    transition-delay: 0s;
}

#toc h2.ui-accordion-header-active {
    background: silver !important;
}

#toc h2:not(.ui-accordion-header-active):hover {
    background: rgb(223, 223, 223) !important;
}

#toc h2 a:hover {
    text-decoration: underline;
}

#toc h2:hover::after {
    content: "expand ▾";
    font-size: 80%;
    float: right;
    margin-top: 0.2em;
    color: silver;
    opacity: 1;
    transition: opacity .5s ease-in-out;
}

#toc h2.ui-accordion-header-active:hover::after {
    opacity: 0;
}

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

div#sec1.hide {
    display: none;
}

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

#toc ul ul {
    margin-bottom: -8px;
}

#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-widget-content {
    background: #ffffff;
    color: #333333;
}

/* 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;
}

.index_button_column {
    float: left;
    width: 30%;
    margin: 0 10px;
    text-align: center;
    font-size: 15px;
    line-height: 25px;
    padding-bottom: 20px;
}

.index_button {
    font-size: 20px;
    text-align: center;
    font-weight: 600;
}

.index_button :link {
    float: left;
    background-color: rgba(0, 0, 0, 0.05);
    border: 1px solid rgba(0, 0, 0, 0.2);
    border-radius: .4rem;
    width: 100%;
    padding-top: 20px;
    padding-bottom: 20px;
}

.index_button :visited {
    float: left;
    background-color: rgba(0, 0, 0, 0.05);
    border: 1px solid rgba(0, 0, 0, 0.2);
    border-radius: .4rem;
    width: 100%;
    padding-top: 20px;
    padding-bottom: 20px;
}

.index_button :hover {
    float: left;
    background-color: rgba(0, 0, 0, 0.07);
    border: 1px solid rgba(0, 0, 0, 0.2);
    border-radius: .4rem;
    width: 100%;
    padding-top: 20px;
    padding-bottom: 20px;
}

.index_button :active {
    float: left;
    background-color: rgba(0, 0, 0, 0.12);
    border: 1px solid rgba(0, 0, 0, 0.2);
    border-radius: .4rem;
    width: 100%;
    padding-top: 20px;
    padding-bottom: 20px;
}

.content_text {
    padding-right: 10px;
    padding-bottom: 20px;
    font-size: 20px;
    line-height: 33px;
}

.content_text .mcomment {
    font-size: 17px;
    font-style: italic;
}

.content_text .mtitle {
    font-size: 23px;
}

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

.mediumauthors {
    font-size: 21px;
    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;
}

table.vc {
    background-color: rgba(159, 125, 140, 0.5);
}

table.vc tbody tr td.tab {
    background-color: rgb(159, 125, 140);
}

/* 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');
}

@font-face {
    font-family: 'JetbrainsMono';
    font-weight: bold;
    font-style: normal;
    src: url('../media/font/CoqBrainsMono/CoqBrainsMono-Regular.otf');
}

@font-face {
    font-family: 'JetbrainsMono';
    font-weight: normal;
    font-style: normal;
    src: url('../media/font/CoqBrainsMono/CoqBrainsMono-Light.otf');
}

@font-face {
    font-family: 'JetbrainsMono';
    font-weight: 700;
    font-style: normal;
    src: url('../media/font/CoqBrainsMono/CoqBrainsMono-Medium.woff2');
}

/* 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;
}