What is Isabelle?
Isabelle is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). See the Isabelle overview.
These site provides general information on Isabelle, more specific information is available from the local sites
See there for information on projects done with Isabelle, mailing list archives, research papers, the Isabelle bibliography, and Isabelle workshops and courses.
Coming soon: Isabelle 2005
New features in the upcoming Isabelle 2005 will include
- New commands for instantiating locales
- New command for finding theorems (by term patterns, as intro/elim/simp rules, etc.)
- New automatic transitivity reasoner
- New command for ad-hoc theory viewing and printing
- Much extended and improved theory of finite sets
- New syntax that will allow > and >= in addition to < and <=
Isabelle 2004
New features in Isabelle 2004 include
- New image HOL4 with imported library from HOL4 system on top of HOL-Complex (about 2500 additional theorems).
- New theory Ring_and_Field with over 250 basic numerical laws, all proved in axiomatic type classes for semirings, rings and fields.
- New locale
ring
for non-commutative rings in HOL-Algebra. - Type
rat
of the rational numbers available in HOL-Complex. - New theory of matrices with an application to linear programming in HOL-Matrix.
- Improved locales (named proof contexts), instantiation of locales.
- Improved handling of linear and partial orders in simplifier.
- New
specification
command for definition by specification. - New Isar command
finalconsts
prevents constants being given a definition later. arith
now generates counterexamples for reals as well.- New
quickcheck
command to search for counterexamples of executable goals. (see HOL/ex/Quickcheck_Examples.thy) - New
refute
command to search for finite countermodels of goals. (see HOL/ex/Refute_Examples.thy) - Presentation and x-symbol enhancements, greek letters and sub/superscripts allowed in identifiers.
Download
The Isabelle distribution is distributed for free and available from several mirror sites. It includes source and binary packages and browsable documentation. You can also browse the Isabelle theory library online.
Use the mailing list isabelle-users@cl.cam.ac.uk and its archive to discuss problems and results. To subscribe, contact Larry Paulson.