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 pages provide general information on Isabelle, more + specific information is available from the local pages +
+ +-
+
+
- Isabelle + at Cambridge + +
- Isabelle + at Munich + +
+ 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 matching rewrite rules +
- Finding theorems by term patterns +
- 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
ringfor non-commutative rings in HOL-Algebra.
+
+ - Type
ratof 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
specificationcommand for definition by specification.
+
+ - New Isar command
finalconstsprevents constants being given a definition later.
+
+ arithnow generates counterexamples for reals as well.
+
+- New
quickcheckcommand + to search for counterexamples of executable goals. + (see HOL/ex/Quickcheck_Examples.thy)
+ - New
refutecommand + 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 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. +
+ +