## What is 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) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction.

## Now available: Isabelle2009-1

Important changes:

- Isabelle tool
`wwwfind`provides web interface for`find_theorems`on a given logic image. - HOL-SMT: proof method
`smt`for a combination of first-order logic with equality, linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors. - HOL-Boogie: an interactive prover back-end for Boogie and VCC.
- HOL: counterexample generator tool Nitpick based on the Kodkod relational model finder.
- HOL: predicate compiler turning inductive into (executable) equational specifications.
- HOL: refined number theory.
- HOL: various parts of multivariate analysis.
- HOL-Library: proof method
`sos`(sum of squares) for nonlinear real arithmetic, based on external semidefinite programming solvers. - HOLCF: new definitional domain package.
- Revised tutorial on locales.
- ML: tacticals for subgoal focus.
- ML: support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
- Parallel checking of nested Isar proofs, with improved scalability up to 8 cores.

See also the cumulative NEWS.

## Download & Support

Isabelle is distributed for free under the BSD license. It includes source and binary packages and browsable documentation, see the installation instructions.

A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.

Support is available by ample documentation and the Isabelle community.