Isabelle

Isabelle is a generic theorem prover. New logics are introduced by specifying their syntax and rules of inference. Proof procedures can be expressed using tactics and tacticals. The latest version, Isabelle-94, is significantly faster than Isabelle-93 and has several other improvements.

Developers: Lawrence C Paulson (University of Cambridge), Tobias Nipkow (Technical University, Munich) and colleagues
Contact:
Number of Sites: many
Line Count: 16,000 (excluding object-logics)
In use: 1986-now
Language: Standard ML
Compilers: Poly/ML, Standard ML of New Jersey
Availability: Isabelle is available from Larry Paulson's FTP area at Cambridge and also from Toby Nipkow's FTP area at Munich.
Related Publications:
- A Gentle Introduction to Isabelle is a short tutorial.
- Introduction to Isabelle explains the basic concepts at length, and gives examples.
- The Isabelle Reference Manual documents nearly all most of Isabelle's facilities, apart from particular object-logics.
- Isabelle's Object-Logics describes the various logics supplied with Isabelle.
- A Fixedpoint Approach to Implementing (Co)inductive Definitions describes the induction/coinductive definition package for ZF.
- Research reports are also available.