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. -
-- This site provides general information on Isabelle, more - specific information is available from the local sites -
- --
-
-
- 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. -
- -Now available: Isabelle2005
-Some highlights:
--
-
- Interpretation of locale expressions in theories, locales, and proof contexts. -
- Substantial library improvements (HOL, HOL-Complex, HOLCF). -
- Proof tools for transitivity reasoning. -
- General
find_theoremscommand (by term patterns, as intro/elim/simp rules etc.).
- - Commands for generating adhoc draft documents. -
- Support for Unicode proof documents (UTF-8). -
- Major internal reorganizations and performance improvements. -
Download
- --Isabelle is distributed for free under the BSD license. It includes -source and binary packages and browsable documentation, see the installation instructions. 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. - Why not subscribe? -
- -