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