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).

Release focus: N/A

Changes:
Initial freshmeat announcement.

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)

 Releases

Version	Focus	Date
2005	Major feature enhancements	21-Mar-2006 22:00
2004	Major feature enhancements	01-May-2004 13:53
2003	Major feature enhancements	19-Jun-2003 19:24
2002	Major feature enhancements	11-Mar-2002 20:07
99-2	Major feature enhancements	16-Feb-2001 13:39
99-1	N/A	10-Oct-2000 16:19