1.1 --- a/NEWS	Fri Sep 18 14:40:24 2009 +0200
     1.2 +++ b/NEWS	Fri Sep 18 18:13:19 2009 +0200
     1.3 @@ -18,6 +18,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New proof method "smt" for a combination of first-order logic
     1.8 +with equality, linear and nonlinear (natural/integer/real)
     1.9 +arithmetic, and fixed-size bitvectors; there is also basic
    1.10 +support for higher-order features (esp. lambda abstractions).
    1.11 +It is an incomplete decision procedure based on external SMT
    1.12 +solvers using the oracle mechanism.
    1.13 +
    1.14  * Reorganization of number theory:
    1.15    * former session NumberTheory now named Old_Number_Theory
    1.16    * new session Number_Theory by Jeremy Avigad; if possible, prefer this.