div.theorem_thmcontent  { border-left: .15rem solid black; }
div.proposition_thmcontent { border-left: .15rem solid black; }
div.lemma_thmcontent     { border-left: .10rem solid black; }
div.corollary_thmcontent { border-left: .10rem solid black; }
div.definition_thmcontent { border-left: .10rem solid #555; }
div.fmlnote_thmcontent   { border-left: .10rem dashed #888; font-size: 0.95rem; }
div.proof_content        { border-left: .08rem solid grey; }

figure.subfloat span.subref { display: none; }

/* alltt (blueprint/CLAUDE.md "The retrospective appendix"): the theme's
   default CSS gives <pre class="verbatim"> whitespace/monospace treatment
   but has no rule for plastex's <div class="alltt"> (used for the Lean
   code excerpts in chapter/retrospective.tex), so without this the
   div's embedded newlines and indentation collapse like ordinary HTML
   text. Mirrors the theme's pre/pre.verbatim rules. */
div.alltt {
    white-space: pre-wrap;
    font-family: monospace;
    margin: 1rem 2rem;
    background-color: #f2f2f2;
    padding: 0.5rem;
}

nav.local_toc ul { font-size: 1.2rem; }

@media (min-width: 1024px) {
    nav.toc       { width: 25vw; }
    div.with-toc  { margin-left: 25vw; }
}

/* Site-wide experiment-disclaimer banner. Mirrored in
   home_page/_includes/head.html for the Jekyll pages. The blueprint
   theme lays body out as a 100vh flex column, so the banner is a
   non-shrinking flex item that pushes the page wrapper down. */
body::before {
    content: "⚠️ An ongoing experiment in autoformalization using LLMs — the prose and Lean code are not yet fully vetted. Take everything here with a grain of salt.";
    display: block;
    flex-shrink: 0;
    padding: 0.4rem 1rem;
    background: #fff3cd;
    color: #664d03;
    border-bottom: 1px solid #ffe69c;
    font-size: 1.1rem;
    text-align: center;
}