# HG changeset patch
# User blanchet
# Date 1394756893 -3600
# Node ID d3967fdc800a9732e20c61c5fad19c0cc691c42c
# Parent  2dbf84ee3deb8b498b83fce8b28213f00ab5d73d
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)

diff -r 2dbf84ee3deb -r d3967fdc800a CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Mar 13 16:07:27 2014 -0700
+++ b/CONTRIBUTORS	Fri Mar 14 01:28:13 2014 +0100
@@ -9,6 +9,15 @@
 * March 2014: René Thiemann
   Improved code generation for multisets.
 
+* Fall 2013 and Winter 2014: Lorenz Panny, Dmitriy Traytel, and
+  Jasmin Blanchette, TUM
+  Various improvements to the BNF-based (co)datatype package, including
+  a more polished "primcorec" command, optimizations, and integration in
+  the "HOL" session.
+
+* Winter 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM
+  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3.
+
 * January 2014: Lars Hupel, TUM
   An improved, interactive simplifier trace with integration into the
   Isabelle/jEdit Prover IDE.
@@ -42,7 +51,7 @@
 
 * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
   Jasmin Blanchette, TUM
-  Various improvements to BNF-based (co)datatype package, including
+  Various improvements to the BNF-based (co)datatype package, including
   "primrec_new" and "primcorec" commands and a compatibility layer.
 
 * Spring and Summer 2013: Ondrej Kuncar, TUM
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: