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: Isabelle2014
Download for Linux
Download for Windows
Download for Mac OS XSome highlights:
- Improved Isabelle/jEdit Prover IDE: navigation, completion, spell-checking, Query panel, Simplifier Trace panel.
- Support for auxiliary files within the Prover IDE, notably Isabelle/ML.
- Support for official Standard ML within the Prover IDE, independently of Isabelle theory and proof development.
- HOL: BNF datatypes and codatatypes within theory Main, with numerous add-on tools.
- HOL tool enhancements: Nitpick, Sledgehammer.
- HOL: internal SAT solver "cdclite" with models and proof traces.
- HOL: updated SMT module, with support for SMT-LIB 2 and recent versions of Z3, as well as CVC3, CVC4.
- HOL: numerous library enhancements: main HOL, HOL-Word, HOL-Multivariate_Analysis, HOL-Probability.
- System integration: improved support of LaTeX on Windows platform.
- Updated and extended manuals: codegen, datatypes, implementation, isar-ref, jedit, system.
See also the cumulative NEWS.
Distribution & Support
Isabelle is distributed for free under the BSD license. It includes source and binary packages and documentation, see the detailed installation instructions. A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.
Support is available by ample documentation, the Isabelle community Wiki, Stack Overflow, and in particular the following mailing lists:
- {isabelle-users} AT [cl.cam.ac.uk] provides a forum for Isabelle users to discuss problems, exchange information, and make announcements. Users of official Isabelle releases should subscribe or see the archive (also available via Google groups and Narkive).
- {isabelle-dev} AT [in.tum.de] covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure. Early adopters of repository versions should subscribe or see the archive (also available at mail-archive.com or gmane.org).