equal
deleted
inserted
replaced
12 |
12 |
13 * Purely algebraic definition of even. Fact generalization and consolidation: |
13 * Purely algebraic definition of even. Fact generalization and consolidation: |
14 nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd |
14 nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd |
15 even_zero_(nat|int) ~> even_zero |
15 even_zero_(nat|int) ~> even_zero |
16 INCOMPATIBILITY. |
16 INCOMPATIBILITY. |
17 |
|
18 *** HOL *** |
|
19 |
17 |
20 * Elimination of fact duplicates: |
18 * Elimination of fact duplicates: |
21 equals_zero_I ~> minus_unique |
19 equals_zero_I ~> minus_unique |
22 diff_eq_0_iff_eq ~> right_minus_eq |
20 diff_eq_0_iff_eq ~> right_minus_eq |
23 INCOMPATIBILITY. |
21 INCOMPATIBILITY. |
49 |
47 |
50 c) Simplification with "diff_def": just drop "diff_def". |
48 c) Simplification with "diff_def": just drop "diff_def". |
51 Consider simplification with algebra_simps or field_simps; |
49 Consider simplification with algebra_simps or field_simps; |
52 or the brute way with |
50 or the brute way with |
53 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". |
51 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". |
|
52 |
|
53 * SUP and INF generalized to conditionally_complete_lattice |
|
54 |
|
55 * Theory Lubs moved HOL image to HOL-Library. It is replaced by |
|
56 Conditionally_Complete_Lattices. INCOMPATIBILITY. |
|
57 |
|
58 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them |
|
59 instead of explicitly stating boundedness of sets. |
|
60 |
54 |
61 |
55 New in Isabelle2013-1 (November 2013) |
62 New in Isabelle2013-1 (November 2013) |
56 ------------------------------------- |
63 ------------------------------------- |
57 |
64 |
58 *** General *** |
65 *** General *** |