[isabelle-dev] NEWS

[Sascha Boehme]

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.