1.1 --- a/NEWS Mon Nov 11 17:34:44 2013 +0100
1.2 +++ b/NEWS Mon Nov 11 17:44:21 2013 +0100
1.3 @@ -1,6 +1,67 @@
1.4 Isabelle NEWS -- history user-relevant changes
1.5 ==============================================
1.6
1.7 +New in this Isabelle version
1.8 +----------------------------
1.9 +
1.10 +*** HOL ***
1.11 +
1.12 +* Qualified constant names Wellfounded.acc, Wellfounded.accp.
1.13 +INCOMPATIBILITY.
1.14 +
1.15 +* Fact generalization and consolidation:
1.16 + neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
1.17 +INCOMPATIBILITY.
1.18 +
1.19 +* Purely algebraic definition of even. Fact generalization and consolidation:
1.20 + nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
1.21 + even_zero_(nat|int) ~> even_zero
1.22 +INCOMPATIBILITY.
1.23 +
1.24 +* Elimination of fact duplicates:
1.25 + equals_zero_I ~> minus_unique
1.26 + diff_eq_0_iff_eq ~> right_minus_eq
1.27 +INCOMPATIBILITY.
1.28 +
1.29 +* Fact name consolidation:
1.30 + diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
1.31 + minus_le_self_iff ~> neg_less_eq_nonneg
1.32 + le_minus_self_iff ~> less_eq_neg_nonpos
1.33 + neg_less_nonneg ~> neg_less_pos
1.34 + less_minus_self_iff ~> less_neg_neg [simp]
1.35 +INCOMPATIBILITY.
1.36 +
1.37 +* More simplification rules on unary and binary minus:
1.38 +add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
1.39 +add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
1.40 +add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
1.41 +le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
1.42 +minus_add_cancel, uminus_add_conv_diff. These correspondingly
1.43 +have been taken away from fact collections algebra_simps and
1.44 +field_simps. INCOMPATIBILITY.
1.45 +
1.46 +To restore proofs, the following patterns are helpful:
1.47 +
1.48 +a) Arbitrary failing proof not involving "diff_def":
1.49 +Consider simplification with algebra_simps or field_simps.
1.50 +
1.51 +b) Lifting rules from addition to subtraction:
1.52 +Try with "using <rule for addition> of [… "- _" …]" by simp".
1.53 +
1.54 +c) Simplification with "diff_def": just drop "diff_def".
1.55 +Consider simplification with algebra_simps or field_simps;
1.56 +or the brute way with
1.57 +"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
1.58 +
1.59 +* SUP and INF generalized to conditionally_complete_lattice
1.60 +
1.61 +* Theory Lubs moved HOL image to HOL-Library. It is replaced by
1.62 +Conditionally_Complete_Lattices. INCOMPATIBILITY.
1.63 +
1.64 +* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
1.65 +instead of explicitly stating boundedness of sets.
1.66 +
1.67 +
1.68 New in Isabelle2013-1 (November 2013)
1.69 -------------------------------------
1.70