1.1 --- a/NEWS	Sat Jul 05 11:19:37 2014 +0200
     1.2 +++ b/NEWS	Sat Jul 05 12:04:25 2014 +0200
     1.3 @@ -221,29 +221,6 @@
     1.4  * The symbol "\<newline>" may be used within char or string literals
     1.5  to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
     1.6  
     1.7 -* Reduced name variants for rules on associativity and commutativity:
     1.8 -
     1.9 -    add_assoc ~> add.assoc
    1.10 -    add_commute ~> add.commute
    1.11 -    add_left_commute ~> add.left_commute
    1.12 -    mult_assoc ~> mult.assoc
    1.13 -    mult_commute ~> mult.commute
    1.14 -    mult_left_commute ~> mult.left_commute
    1.15 -    nat_add_assoc ~> add.assoc
    1.16 -    nat_add_commute ~> add.commute
    1.17 -    nat_add_left_commute ~> add.left_commute
    1.18 -    nat_mult_assoc ~> mult.assoc
    1.19 -    nat_mult_commute ~> mult.commute
    1.20 -    eq_assoc ~> iff_assoc
    1.21 -    eq_left_commute ~> iff_left_commute
    1.22 -
    1.23 -INCOMPATIBILITY.
    1.24 -
    1.25 -* Removed collections add_ac and mult_ac.  Prefer ac_simps instead,
    1.26 -or specify rules (add|mult).(assoc|commute|left_commute) individually.
    1.27 -
    1.28 -INCOMPATIBILITY.
    1.29 -
    1.30  * Qualified String.implode and String.explode.  INCOMPATIBILITY.
    1.31  
    1.32  * Simplifier: Enhanced solver of preconditions of rewrite rules can
    1.33 @@ -601,6 +578,29 @@
    1.34  
    1.35  INCOMPATIBILITY.
    1.36  
    1.37 +* Reduced name variants for rules on associativity and commutativity:
    1.38 +
    1.39 +    add_assoc ~> add.assoc
    1.40 +    add_commute ~> add.commute
    1.41 +    add_left_commute ~> add.left_commute
    1.42 +    mult_assoc ~> mult.assoc
    1.43 +    mult_commute ~> mult.commute
    1.44 +    mult_left_commute ~> mult.left_commute
    1.45 +    nat_add_assoc ~> add.assoc
    1.46 +    nat_add_commute ~> add.commute
    1.47 +    nat_add_left_commute ~> add.left_commute
    1.48 +    nat_mult_assoc ~> mult.assoc
    1.49 +    nat_mult_commute ~> mult.commute
    1.50 +    eq_assoc ~> iff_assoc
    1.51 +    eq_left_commute ~> iff_left_commute
    1.52 +
    1.53 +INCOMPATIBILITY.
    1.54 +
    1.55 +* Removed collections add_ac and mult_ac.  Prefer ac_simps instead,
    1.56 +or specify rules (add|mult).(assoc|commute|left_commute) individually.
    1.57 +
    1.58 +INCOMPATIBILITY.
    1.59 +
    1.60  * Elimination of fact duplicates:
    1.61      equals_zero_I ~> minus_unique
    1.62      diff_eq_0_iff_eq ~> right_minus_eq