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: Isabelle2019 (June 2019)
Download for Linux
Download for Windows
Download for macOSSome notable changes:
- Improved Isabelle DejaVu font collection, suitable for text and GUI.
- Various Isabelle/jEdit improvements, with virtual file-system access to sessions and exports.
- Improved headless PIDE session (and server).
- HOL: export_code now generates logical files in the theory and session context, e.g. browsable as
isabelle-export:in Isabelle/jEdit. - HOL: various syntax and library improvements.
- HOL libraries: better organization and much more material in HOL-Algebra, HOL-Analysis, HOL-Homology
- Isabelle/ML environments for separate SML applications.
- Isabelle/Haskell library for implementation of Isabelle/PIDE backends.
- Installation management for Haskell (Stack) and OCaml (OPAM).
- Update to current Java 11 and Poly/ML 5.8 with better scalability.
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.
- {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 development snapshots or repository versions should subscribe or see the archive (also available at mail-archive.com).