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

Isabelle 2004

New features in Isabelle 2004 include

[Complete Changelog]

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.