Isabelle

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.

Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel).
Features:
- Experimental Prover IDE based on Isabelle/Scala and jEdit.
- Coercive subtyping (configured in HOL/Complex_Main).
- HOL code generation: Scala as another target language.
- HOL: partial_function definitions.
- HOL: various tool enhancements, including Quickcheck, Nitpick, Sledgehammer, SMT integration.
- HOL: various additions to theory library, including HOL-Algebra, Imperative_HOL, Multivariate_Analysis, Probability.
- HOLCF: reorganization of library and related tools.
- HOL/SPARK: interactive proof environment for verification conditions generated by the SPARK Ada program verifier.
- Improved Isabelle/Isar implementation manual (covering Isabelle/ML).