NEWS
changeset 56118 d3967fdc800a
parent 56076 e52fc7c37ed3
child 56148 d94d6a9178b5
     1.1 --- a/NEWS	Thu Mar 13 16:07:27 2014 -0700
     1.2 +++ b/NEWS	Fri Mar 14 01:28:13 2014 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4      BNF/Equiv_Relations_More.thy
     1.5    INCOMPATIBILITY.
     1.6  
     1.7 -* New datatype package:
     1.8 +* New (co)datatype package:
     1.9    * "primcorec" is fully implemented.
    1.10    * Renamed commands:
    1.11        datatype_new_compat ~> datatype_compat
    1.12 @@ -223,7 +223,14 @@
    1.13  * Theory reorganizations:
    1.14    * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
    1.15  
    1.16 +* SMT module:
    1.17 +  * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
    1.18 +    and supports recent versions of Z3 (e.g., 4.3). The new proof method is
    1.19 +    called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and
    1.20 +    elsewhere.
    1.21 +
    1.22  * Sledgehammer:
    1.23 +  - New prover "z3_new" with support for Isar proofs
    1.24    - New option:
    1.25        smt_proofs
    1.26    - Renamed options: