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) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction.
Now available: Isabelle2009
Some notable improvements:
- Complete re-implementation of locales, with proper support for local syntax, and more general locale expressions.
- New find_consts and find_theorems facilities, together with "auto solve" feature of toplevel goal statements.
- HOL: reorganization of main logic images.
- HOL: improved implementation of Sledgehammer, based on generic ATP manager; support for remote ATPs.
- HOL: numerous library improvements.
- Updated and extended versions of main reference manuals.
- Simplified arrangement of Isabelle startup scripts and settings directory.
- Simplified programming interfaces for all Isar language elements.
- General high-level support for concurrent ML programming.
- Parallel proof checking within Isar theories.
- Haskabelle importer from Haskell source files to Isar theories.
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.