equal
deleted
inserted
replaced
378 called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and |
378 called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and |
379 elsewhere. |
379 elsewhere. |
380 |
380 |
381 * Sledgehammer: |
381 * Sledgehammer: |
382 - New prover "z3_new" with support for Isar proofs |
382 - New prover "z3_new" with support for Isar proofs |
|
383 - MaSh overhaul: |
|
384 - A new SML-based learning engine eliminates the dependency on Python |
|
385 and increases performance and reliability. See the Sledgehammer |
|
386 documentation for details. |
383 - New option: |
387 - New option: |
384 smt_proofs |
388 smt_proofs |
385 - Renamed options: |
389 - Renamed options: |
386 isar_compress ~> compress_isar |
390 isar_compress ~> compress_isar |
387 isar_try0 ~> try0_isar |
391 isar_try0 ~> try0_isar |