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)

---