# HG changeset patch # User nipkow # Date 1233220105 -3600 # Node ID 16c8799e6a21d36f21a9af848b215cbe87b7e440 # Parent c82a76a66e806aeadb50610811df4250f820fbd2# Parent 07f3da9fd2a00041843aec9e29575e445a975f33 merged diff -r 07f3da9fd2a0 -r 16c8799e6a21 NEWS --- a/NEWS Thu Jan 29 10:07:43 2009 +0100 +++ b/NEWS Thu Jan 29 10:08: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