[isabelle-dev] NEWS

Sascha Boehme boehmes at in.tum.de
Fri Sep 25 11:05:57 CEST 2009

New proof method "smt" for a combination of first-order logic
with equality, linear and nonlinear (natural/integer/real)
arithmetic, and fixed-size bitvectors; there is also basic
support for higher-order features (esp. lambda abstractions).
It is an incomplete decision procedure based on external SMT
solvers using the oracle mechanism.

More information about the isabelle-dev mailing list