Oberwolfach References on Mathematical Software



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


Isabelle is a joint project between Lawrence C. Paulson (University of Cambridge, UK) and Tobias Nipkow (Technical University of Munich, Germany).


Isabelle is distributed freely as Open Source Software BSD license.



projectstatus   officially approved by the authors

Available via

Operating Systems

Programming Languages


Free downloadable

Technical Category

Specialized system

Download pdf description

Contact and Support: it@mfo.de, Imprint/Impressum


Valid XHTML 1.0 Transitional CSS is´valid!