Theory Collections
Jump to navigation
Jump to search
- The Isabelle Library
- The collection of theories included in Isabelle
- AFP: The Archive of Formal Proofs
- THE collection of Isabelle theories outside of Isabelle itself
- Projects
- An (incomplete) list of past and present projects undertaken using Isabelle.
- IsaFoR: Isabelle Formalization of Rewriting
- A proof library on abstract rewriting and first-order term rewriting with main focus termination. Using Isabelle's code generator the termination proof certifier CeTA can be generated from IsaFoR.
- IsaFoL Isabelle Formalization of Logic
- A proof library on logic.
- HOLCF-Prelude: A Formalization of Haskell's Standard Prelude in HOLCF
- The project is currently very preliminary and contributions are most welcome.
- IsarMathLib: A library of formalized mathematics for Isabelle/Isar
- A formalization of algebra and general topology in Isabelle/ZF
- Isabelle Repository for Relational and Algebraic Methods
- Isabelle Repository for Relational and Algebraic Methods