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 is Isabelle-99.
Lawrence C Paulson (University of Cambridge),
Tobias Nipkow (Technical University, Munich) and colleagues
Lawrence C. Paulson
University of Cambridge
Cambridge CB2 3QG
- Number of Sites:
- Line Count:
43,000+ (excluding object-logics)
- In use:
Poly/ML, Standard ML of New Jersey, ML Works
Isabelle is available from
and other mirror sites.
- Related Publications:
Documentation is included with the distribution.
Many research reports can be found on the