NEWS
changeset 54250 7d2544dd3988
parent 54230 b1d955791529
child 54264 27501a51d847
     1.1 --- a/NEWS	Mon Nov 04 20:10:06 2013 +0100
     1.2 +++ b/NEWS	Mon Nov 04 20:10:09 2013 +0100
     1.3 @@ -24,6 +24,10 @@
     1.4  
     1.5  * Fact name consolidation:
     1.6      diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
     1.7 +    minus_le_self_iff ~> neg_less_eq_nonneg
     1.8 +    le_minus_self_iff ~> less_eq_neg_nonpos
     1.9 +    neg_less_nonneg ~> neg_less_pos
    1.10 +    less_minus_self_iff ~> less_neg_neg [simp]
    1.11  INCOMPATIBILITY.
    1.12  
    1.13  * More simplification rules on unary and binary minus:
    1.14 @@ -48,7 +52,6 @@
    1.15  or the brute way with
    1.16  "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
    1.17  
    1.18 -
    1.19  New in Isabelle2013-1 (November 2013)
    1.20  -------------------------------------
    1.21