diff -r 2dbf84ee3deb -r d3967fdc800a NEWS
--- a/NEWS	Thu Mar 13 16:07:27 2014 -0700
+++ b/NEWS	Fri Mar 14 01:28:13 2014 +0100
@@ -162,7 +162,7 @@
     BNF/Equiv_Relations_More.thy
   INCOMPATIBILITY.
 
-* New datatype package:
+* New (co)datatype package:
   * "primcorec" is fully implemented.
   * Renamed commands:
       datatype_new_compat ~> datatype_compat
@@ -223,7 +223,14 @@
 * Theory reorganizations:
   * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
 
+* SMT module:
+  * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
+    and supports recent versions of Z3 (e.g., 4.3). The new proof method is
+    called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and
+    elsewhere.
+
 * Sledgehammer:
+  - New prover "z3_new" with support for Isar proofs
   - New option:
       smt_proofs
   - Renamed options: