- HOL
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).
- FOL
First-Order Logic with some variations: single-sorted vs. many-sorted
(polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs.
set-theory (ZF).
- Pure
The Pure logical framework.
Isabelle/Pure is a version of intuitionistic higher-order logic that
expresses rules for Natural Deduction declaratively.
- Misc
Miscellaneous object-logics, tools, and experiments.
- Doc
Sources of Documentation.
- Unsorted
Sessions without 'chapter' declaration.