diff -r c0056c2c1d17 -r 42865636d006 NEWS
--- a/NEWS	Fri Sep 18 14:40:24 2009 +0200
+++ b/NEWS	Fri Sep 18 18:13:19 2009 +0200
@@ -18,6 +18,13 @@
 
 *** HOL ***
 
+* 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.
+
 * Reorganization of number theory:
   * former session NumberTheory now named Old_Number_Theory
   * new session Number_Theory by Jeremy Avigad; if possible, prefer this.