--- 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: