About:
Isabelle is a popular generic theorem prover developed at Cambridge University and TU Munich. Existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications. Isabelle may also serve as framework for rapid prototyping of deductive systems. It comes with a large library including Isabelle/HOL (classical higher-order logic), Isabelle/HOLCF (Scott's Logic for Computable Functions with HOL), Isabelle/FOL (classical and intuitionistic first-order logic), and Isabelle/ZF (Zermelo-Fraenkel set theory on top of FOL).

Author:
The Isabelle Team <isabelle __dash__ enquiries __at__ cl __dot__ cam __dot__ ac __dot__ uk> [contact developer]

Rating:	reset 1 2 3 4 5 6 7 8 9 10
8.40/10.00 (1 vote)

Homepage:
http://isabelle.in.tum.de/
Changelog:
http://isabelle.in.tum.de/dist/Isabelle/NEWS
Mirror site:
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

Trove categories: [change]

[Development Status]		5 - Production/Stable
[Environment]		Console (Text Based), X11 Applications
[License]		OSI Approved :: BSD License (revised)
[Operating System]		MacOS X, POSIX :: Linux, POSIX :: SunOS/Solaris
[Programming Language]		ML
[Topic]		Education, Scientific/Engineering :: Mathematics

Dependencies: [change]
Proof General (Default branch) (recommended)
[download links]

 Branches

Branch	Version	Last release	License	URLs
Default	2005	21-Mar-2006	BSD License (revised)