--- /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."