--- a/NEWS Sat Jul 05 11:19:37 2014 +0200
+++ b/NEWS Sat Jul 05 12:04:25 2014 +0200
@@ -221,29 +221,6 @@
* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
-* Reduced name variants for rules on associativity and commutativity:
-
- add_assoc ~> add.assoc
- add_commute ~> add.commute
- add_left_commute ~> add.left_commute
- mult_assoc ~> mult.assoc
- mult_commute ~> mult.commute
- mult_left_commute ~> mult.left_commute
- nat_add_assoc ~> add.assoc
- nat_add_commute ~> add.commute
- nat_add_left_commute ~> add.left_commute
- nat_mult_assoc ~> mult.assoc
- nat_mult_commute ~> mult.commute
- eq_assoc ~> iff_assoc
- eq_left_commute ~> iff_left_commute
-
-INCOMPATIBILITY.
-
-* Removed collections add_ac and mult_ac. Prefer ac_simps instead,
-or specify rules (add|mult).(assoc|commute|left_commute) individually.
-
-INCOMPATIBILITY.
-
* Qualified String.implode and String.explode. INCOMPATIBILITY.
* Simplifier: Enhanced solver of preconditions of rewrite rules can
@@ -601,6 +578,29 @@
INCOMPATIBILITY.
+* Reduced name variants for rules on associativity and commutativity:
+
+ add_assoc ~> add.assoc
+ add_commute ~> add.commute
+ add_left_commute ~> add.left_commute
+ mult_assoc ~> mult.assoc
+ mult_commute ~> mult.commute
+ mult_left_commute ~> mult.left_commute
+ nat_add_assoc ~> add.assoc
+ nat_add_commute ~> add.commute
+ nat_add_left_commute ~> add.left_commute
+ nat_mult_assoc ~> mult.assoc
+ nat_mult_commute ~> mult.commute
+ eq_assoc ~> iff_assoc
+ eq_left_commute ~> iff_left_commute
+
+INCOMPATIBILITY.
+
+* Removed collections add_ac and mult_ac. Prefer ac_simps instead,
+or specify rules (add|mult).(assoc|commute|left_commute) individually.
+
+INCOMPATIBILITY.
+
* Elimination of fact duplicates:
equals_zero_I ~> minus_unique
diff_eq_0_iff_eq ~> right_minus_eq