The Isabelle Library

Higher-Order Logic

- HOL (Higher-Order Logic)
- HOLCF (Higher-Order Logic of Computable Functions)

First-Order Logic

- FOL (Many-sorted First-Order Logic)
- ZF (Set Theory)
- 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)
- Cube (The Lambda Cube)