updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
authorblanchet
Fri Mar 14 01:28:13 2014 +0100 (2014-03-14)
changeset 56118d3967fdc800a
parent 56117 2dbf84ee3deb
child 56119 2e44053fee87
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Thu Mar 13 16:07:27 2014 -0700
     1.2 +++ b/CONTRIBUTORS	Fri Mar 14 01:28:13 2014 +0100
     1.3 @@ -9,6 +9,15 @@
     1.4  * March 2014: René Thiemann
     1.5    Improved code generation for multisets.
     1.6  
     1.7 +* Fall 2013 and Winter 2014: Lorenz Panny, Dmitriy Traytel, and
     1.8 +  Jasmin Blanchette, TUM
     1.9 +  Various improvements to the BNF-based (co)datatype package, including
    1.10 +  a more polished "primcorec" command, optimizations, and integration in
    1.11 +  the "HOL" session.
    1.12 +
    1.13 +* Winter 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM
    1.14 +  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3.
    1.15 +
    1.16  * January 2014: Lars Hupel, TUM
    1.17    An improved, interactive simplifier trace with integration into the
    1.18    Isabelle/jEdit Prover IDE.
    1.19 @@ -42,7 +51,7 @@
    1.20  
    1.21  * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
    1.22    Jasmin Blanchette, TUM
    1.23 -  Various improvements to BNF-based (co)datatype package, including
    1.24 +  Various improvements to the BNF-based (co)datatype package, including
    1.25    "primrec_new" and "primcorec" commands and a compatibility layer.
    1.26  
    1.27  * Spring and Summer 2013: Ondrej Kuncar, TUM
     2.1 --- a/NEWS	Thu Mar 13 16:07:27 2014 -0700
     2.2 +++ b/NEWS	Fri Mar 14 01:28:13 2014 +0100
     2.3 @@ -162,7 +162,7 @@
     2.4      BNF/Equiv_Relations_More.thy
     2.5    INCOMPATIBILITY.
     2.6  
     2.7 -* New datatype package:
     2.8 +* New (co)datatype package:
     2.9    * "primcorec" is fully implemented.
    2.10    * Renamed commands:
    2.11        datatype_new_compat ~> datatype_compat
    2.12 @@ -223,7 +223,14 @@
    2.13  * Theory reorganizations:
    2.14    * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
    2.15  
    2.16 +* SMT module:
    2.17 +  * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
    2.18 +    and supports recent versions of Z3 (e.g., 4.3). The new proof method is
    2.19 +    called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and
    2.20 +    elsewhere.
    2.21 +
    2.22  * Sledgehammer:
    2.23 +  - New prover "z3_new" with support for Isar proofs
    2.24    - New option:
    2.25        smt_proofs
    2.26    - Renamed options: