equal
deleted
inserted
replaced
22 * Quickcheck: |
22 * Quickcheck: |
23 |
23 |
24 - added an optimisation for equality premises. |
24 - added an optimisation for equality premises. |
25 It is switched on by default, and can be switched off by setting |
25 It is switched on by default, and can be switched off by setting |
26 the configuration quickcheck_optimise_equality to false. |
26 the configuration quickcheck_optimise_equality to false. |
|
27 |
|
28 * The SMT solver Z3 has now by default a restricted set of directly |
|
29 supported features. For the full set of features (div/mod, nonlinear |
|
30 arithmetic, datatypes/records) with potential proof reconstruction |
|
31 failures, enable the configuration option "z3_with_extensions". |
|
32 Minor INCOMPATIBILITY. |
27 |
33 |
28 New in Isabelle2012 (May 2012) |
34 New in Isabelle2012 (May 2012) |
29 ------------------------------ |
35 ------------------------------ |
30 |
36 |
31 *** General *** |
37 *** General *** |