--- a/NEWS Thu Aug 03 14:53:57 2006 +0200
+++ b/NEWS Thu Aug 03 14:57:26 2006 +0200
@@ -521,7 +521,13 @@
*** HOL-Algebra ***
* Method algebra is now set up via an attribute. For examples see CRing.thy.
- INCOMPATIBILITY: the method is now weaker on combinations of algebraic structures.
+ INCOMPATIBILITY: the method is now weaker on combinations of algebraic
+ structures.
+
+* Formalisation of ideals and the quotient construction over rings, contributed
+ by Stephan Hohe.
+
+* Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY.
*** HOL-Complex ***