The Isabelle2017 Library
Higher-Order Logic
HOL (Higher-Order Logic)
is a version of classical higher-order logic resembling that of the
HOL System
.
First-Order Logic
FOL (Many-sorted First-Order Logic)
provides basic classical and intuitionistic first-order logic. It is polymorphic.
ZF (Set Theory)
offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
CCL (Classical Computational Logic)
LCF (Logic of Computable Functions)
FOLP (FOL with Proof Terms)
Miscellaneous
Sequents (first-order, modal and linear logics)
CTT (Constructive Type Theory)
is an extensional version of Martin-Löf's Type Theory.
Cube (The Lambda Cube)
The Pure logical framework
Sources of Documentation