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 was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction.
Now available: Isabelle2016
Download for Linux
Download for Windows
Download for Mac OS XSome highlights:
- Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel and more asynchronous task management within the prover/GUI.
- Additional Isar language elements for structured statements and proofs.
- Document language refinements, with Markdown-like text structure.
- More Isabelle symbols in theory and document sources.
- Pure/HOL: uniform treatment of overloaded constant definitions versus type definitions; upgrade of HOL typedef to definitional principle.
- HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
- HOL library additions and improvements, notably HOL-Multivariate_Analysis, HOL-Probability, HOL-Data_Structures.
- Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard ML), per-thread profiling, native Windows version (32bit and 64bit).
See also the cumulative NEWS.
Distribution & Support
Isabelle is distributed for free under a conglomerate of open-source licenses, but the main code-base is subject to BSD-style regulations. The application bundles include 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).