# HG changeset patch
# User nipkow
# Date 1233175765 -3600
# Node ID c82a76a66e806aeadb50610811df4250f820fbd2
# Parent  cbe35f4f04f88c88dfef0c2fadff60770418299d
-

diff -r cbe35f4f04f8 -r c82a76a66e80 NEWS
--- a/NEWS	Wed Jan 28 17:12:25 2009 +0100
+++ b/NEWS	Wed Jan 28 21:49:25 2009 +0100
@@ -314,6 +314,11 @@
 Occasionally this is more convenient than the old fold combinator which is
 now defined in terms of the new one and renamed to fold_image.
 
+* HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas "group_simps" and
+"ring_simps" have been replaced by "algebra_simps" (which can be extended with
+further lemmas!). At the moment both still exist but the former will disappear
+at some point.
+
 * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been
 moved to separate class dvd in Ring_and_Field; a couple of lemmas on
 dvd has been generalized to class comm_semiring_1.  Likewise a bunch