# HG changeset patch
# User wenzelm
# Date 1661542548 -7200
# Node ID ca73ced9e630872e4e7b9261ea87bcb2a0bd0c26
# Parent  ff2e67d73592aba8999479b759eb2d623021ea3d
provide chapter descriptions, based on lib/html/library_index_content.template;

diff -r ff2e67d73592 -r ca73ced9e630 ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ROOT	Fri Aug 26 21:35:48 2022 +0200
@@ -0,0 +1,55 @@
+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."