NEWS
changeset 54230 b1d955791529
parent 54228 229282d53781
child 54250 7d2544dd3988
     1.1 --- a/NEWS	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/NEWS	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -15,6 +15,39 @@
     1.4      even_zero_(nat|int) ~> even_zero
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Elimination of fact duplicates:
    1.10 +    equals_zero_I ~> minus_unique
    1.11 +    diff_eq_0_iff_eq ~> right_minus_eq
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14 +* Fact name consolidation:
    1.15 +    diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
    1.16 +INCOMPATIBILITY.
    1.17 +
    1.18 +* More simplification rules on unary and binary minus:
    1.19 +add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
    1.20 +add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
    1.21 +add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
    1.22 +le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
    1.23 +minus_add_cancel, uminus_add_conv_diff.  These correspondingly
    1.24 +have been taken away from fact collections algebra_simps and
    1.25 +field_simps.  INCOMPATIBILITY.
    1.26 +
    1.27 +To restore proofs, the following patterns are helpful:
    1.28 +
    1.29 +a) Arbitrary failing proof not involving "diff_def":
    1.30 +Consider simplification with algebra_simps or field_simps.
    1.31 +
    1.32 +b) Lifting rules from addition to subtraction:
    1.33 +Try with "using <rule for addition> of [… "- _" …]" by simp".
    1.34 +
    1.35 +c) Simplification with "diff_def": just drop "diff_def".
    1.36 +Consider simplification with algebra_simps or field_simps;
    1.37 +or the brute way with
    1.38 +"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
    1.39 +
    1.40  
    1.41  New in Isabelle2013-1 (November 2013)
    1.42  -------------------------------------