Tutorials and manuals for Isabelle2009-1
Learning and using Isabelle
- Tutorial on Isabelle/HOL
- What's in Main
- Tutorial on Isar
- Tutorial on Locales
- Tutorial on Type Classes
- Tutorial on Function Definitions
- Tutorial on Code Generation
- User's Guide to Nitpick in Isabelle/HOL
- LaTeX Sugar for Isabelle documents
Reference Manuals
- The Isabelle/Isar Reference Manual
- The Isabelle/Isar Implementation Manual
- The Isabelle System Manual
Old Manuals (outdated)
- Old Introduction to Isabelle
- Old Isabelle Reference Manual
- Isabelle's Logics: overview and misc logics
- Isabelle's Logics: HOL
- Isabelle's Logics: FOL and ZF
- (Co)Inductive Definitions in ZF
Theory libraries for Isabelle2009-1
- Higher-Order Logic
-
- HOL (Higher-Order Logic) is a version of classical higher-order logic resembling that of the HOL System.
- HOLCF (Higher-Order Logic of Computable Functions) adds Scott's Logic for Computable Functions (domain theory) to HOL.
- 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)