Theory Collections

From Isabelle Community Wiki
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
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