ROOT

provide chapter descriptions, based on lib/html/library_index_content.template;

chapter_definition HOL
  description "
    Higher-Order Logic.

    Isabelle/HOL is a version of classical higher-order logic resembling
    that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL).
  "

chapter_definition FOL
  description "
    Many-sorted First-Order Logic.

    Isabelle/FOL provides basic classical and intuitionistic first-order logic.
    It is polymorphic.
  "

chapter_definition ZF
  description "
    Isabelle/ZF (Set Theory) offers a formulation of Zermelo-Fraenkel set theory
    on top of Isabelle/FOL.
  "

chapter_definition CCL
  description "Classical Computational Logic."

chapter_definition LCF
  description "Logic of Computable Functions."

chapter_definition FOLP
  description "FOL with Proof Terms."

chapter_definition Sequents
  description "First-order, modal and linear logics."

chapter_definition CTT
  description "
    Constructive Type Theory: an extensional version of Martin-Löf's Type Theory.
  "

chapter_definition Cube
  description "Barendregt's Lambda Cube."

chapter_definition Pure
  description "
    The Pure logical framework.

    Isabelle/Pure is a version of intuitionistic higher-order logic that
    expresses rules for Natural Deduction declaratively.
  "

chapter_definition Doc
  description "Sources of Documentation."

chapter_definition Tools
  description "Miscellaneous tools."