equal
deleted
inserted
replaced
22 diff_eq_0_iff_eq ~> right_minus_eq |
22 diff_eq_0_iff_eq ~> right_minus_eq |
23 INCOMPATIBILITY. |
23 INCOMPATIBILITY. |
24 |
24 |
25 * Fact name consolidation: |
25 * Fact name consolidation: |
26 diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus |
26 diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus |
|
27 minus_le_self_iff ~> neg_less_eq_nonneg |
|
28 le_minus_self_iff ~> less_eq_neg_nonpos |
|
29 neg_less_nonneg ~> neg_less_pos |
|
30 less_minus_self_iff ~> less_neg_neg [simp] |
27 INCOMPATIBILITY. |
31 INCOMPATIBILITY. |
28 |
32 |
29 * More simplification rules on unary and binary minus: |
33 * More simplification rules on unary and binary minus: |
30 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1, |
34 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1, |
31 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, |
35 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, |
45 |
49 |
46 c) Simplification with "diff_def": just drop "diff_def". |
50 c) Simplification with "diff_def": just drop "diff_def". |
47 Consider simplification with algebra_simps or field_simps; |
51 Consider simplification with algebra_simps or field_simps; |
48 or the brute way with |
52 or the brute way with |
49 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". |
53 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". |
50 |
|
51 |
54 |
52 New in Isabelle2013-1 (November 2013) |
55 New in Isabelle2013-1 (November 2013) |
53 ------------------------------------- |
56 ------------------------------------- |
54 |
57 |
55 *** General *** |
58 *** General *** |