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: Isabelle2008
Some notable improvements:
- HOL: significant speedup of Metis prover; proper support for multithreading.
- HOL: new version of primrec command supporting type-inference and local theory targets.
- HOL: improved support for termination proofs of recursive function definitions.
- New local theory targets for class instantiation and overloading.
- Support for named dynamic lists of theorems.
- Simple TTY interface with command-line editing.
- Improved support for the Cygwin platform.
- Support for Poly/ML 5.2 with improved handling of multithreading and external processes.
- Reorganized and updated version of Isabelle/Isar Reference Manual.
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.