1 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
2 ============================================== |
|
3 |
|
4 New in this Isabelle version |
|
5 ---------------------------- |
|
6 |
|
7 *** HOL *** |
|
8 |
|
9 * Qualified constant names Wellfounded.acc, Wellfounded.accp. |
|
10 INCOMPATIBILITY. |
|
11 |
|
12 * Fact generalization and consolidation: |
|
13 neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 |
|
14 INCOMPATIBILITY. |
|
15 |
|
16 * Purely algebraic definition of even. Fact generalization and consolidation: |
|
17 nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd |
|
18 even_zero_(nat|int) ~> even_zero |
|
19 INCOMPATIBILITY. |
|
20 |
|
21 * Elimination of fact duplicates: |
|
22 equals_zero_I ~> minus_unique |
|
23 diff_eq_0_iff_eq ~> right_minus_eq |
|
24 INCOMPATIBILITY. |
|
25 |
|
26 * Fact name consolidation: |
|
27 diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus |
|
28 minus_le_self_iff ~> neg_less_eq_nonneg |
|
29 le_minus_self_iff ~> less_eq_neg_nonpos |
|
30 neg_less_nonneg ~> neg_less_pos |
|
31 less_minus_self_iff ~> less_neg_neg [simp] |
|
32 INCOMPATIBILITY. |
|
33 |
|
34 * More simplification rules on unary and binary minus: |
|
35 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1, |
|
36 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, |
|
37 add_minus_cancel, diff_add_cancel, le_add_same_cancel1, |
|
38 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, |
|
39 minus_add_cancel, uminus_add_conv_diff. These correspondingly |
|
40 have been taken away from fact collections algebra_simps and |
|
41 field_simps. INCOMPATIBILITY. |
|
42 |
|
43 To restore proofs, the following patterns are helpful: |
|
44 |
|
45 a) Arbitrary failing proof not involving "diff_def": |
|
46 Consider simplification with algebra_simps or field_simps. |
|
47 |
|
48 b) Lifting rules from addition to subtraction: |
|
49 Try with "using <rule for addition> of [… "- _" …]" by simp". |
|
50 |
|
51 c) Simplification with "diff_def": just drop "diff_def". |
|
52 Consider simplification with algebra_simps or field_simps; |
|
53 or the brute way with |
|
54 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". |
|
55 |
|
56 * SUP and INF generalized to conditionally_complete_lattice |
|
57 |
|
58 * Theory Lubs moved HOL image to HOL-Library. It is replaced by |
|
59 Conditionally_Complete_Lattices. INCOMPATIBILITY. |
|
60 |
|
61 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them |
|
62 instead of explicitly stating boundedness of sets. |
|
63 |
3 |
64 |
4 New in Isabelle2013-1 (November 2013) |
65 New in Isabelle2013-1 (November 2013) |
5 ------------------------------------- |
66 ------------------------------------- |
6 |
67 |
7 *** General *** |
68 *** General *** |