What is Isabelle?
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel). See the Isabelle overview for a brief introduction.
Now available: Isabelle2009-2
Notable changes:
- Explicit proof terms for type class reasoning.
- Robust treatment of concrete syntax for different logical entities; mixfix syntax in local proof context.
- Type declarations and notation within local theory context.
- HOL: package for quotient types.
- HOL code generation: simple concept for abstract datatypes obeying invariants (e.g. red-black trees).
- HOL: new development of the Reals using Cauchy Sequences.
- HOL: reorganization of abstract algebra type class hierarchy.
- HOL: substantial reorganization of main library and related tools.
- HOLCF: reorganization of 'domain' package.
See also the cumulative NEWS.
Download & Support
Isabelle is distributed for free under the BSD license. It includes source and binary packages and browsable documentation, see the installation instructions.
A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.
Support is available by ample documentation and the Isabelle community.