--- a/NEWS Fri Mar 17 09:57:25 2006 +0100
+++ b/NEWS Fri Mar 17 10:04:27 2006 +0100
@@ -346,7 +346,7 @@
25 like -->); output depends on the "iff" print_mode, the default is
"A = B" (with priority 50).
-* Renamed some (legacy-named) constants in HOL.thy and Orderings.thy:
+* Renamed constants in HOL.thy and Orderings.thy:
op + ~> HOL.plus
op - ~> HOL.minus
uminus ~> HOL.uminus
@@ -385,6 +385,8 @@
* Theorem Cons_eq_map_conv no longer has attribute `simp'.
+* Theorem setsum_mult renamed to setsum_right_distrib.
+
* Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
'rule' method.