NEWS
changeset 57245 f6bf6d5341ee
parent 57241 7fca4159117f
child 57246 62746a41cc0c
     1.1 --- a/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:10:12 2014 +0200
     1.3 @@ -387,7 +387,7 @@
     1.4      SMT-LIB 2 and quantifiers.
     1.5  
     1.6  * Sledgehammer:
     1.7 -  - New prover "z3_new" with support for Isar proofs
     1.8 +  - "z3" can now produce Isar proofs
     1.9    - MaSh overhaul:
    1.10        - New SML-based learning engines eliminate the dependency on Python
    1.11          and increase performance and reliability.
    1.12 @@ -399,8 +399,8 @@
    1.13    - New option:
    1.14        smt_proofs
    1.15    - Renamed options:
    1.16 -      isar_compress ~> compress_isar
    1.17 -      isar_try0 ~> try0_isar
    1.18 +      isar_compress ~> compress
    1.19 +      isar_try0 ~> try0
    1.20      INCOMPATIBILITY.
    1.21  
    1.22  * Metis: