diff -r 2ddc7edce107 -r e682bb587071 NEWS
--- a/NEWS	Mon Feb 08 14:04:51 2010 +0100
+++ b/NEWS	Mon Feb 08 14:08:32 2010 +0100
@@ -12,7 +12,7 @@
 
 *** HOL ***
 
-* more consistent naming of type classes involving orderings (and lattices):
+* More consistent naming of type classes involving orderings (and lattices):
 
     lower_semilattice                   ~> semilattice_inf
     upper_semilattice                   ~> semilattice_sup
@@ -33,12 +33,6 @@
     pordered_ring_abs                   ~> ordered_ring_abs
     pordered_semiring                   ~> ordered_semiring
 
-    lordered_ab_group_add               ~> lattice_ab_group_add
-    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
-    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
-    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
-    lordered_ring                       ~> lattice_ring
-
     ordered_ab_group_add                ~> linordered_ab_group_add
     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
@@ -58,6 +52,15 @@
     ordered_semiring_1_strict           ~> linordered_semiring_1_strict
     ordered_semiring_strict             ~> linordered_semiring_strict
 
+  The following slightly odd type classes have been moved to
+  a separate theory Library/Lattice_Algebras.thy:
+
+    lordered_ab_group_add               ~> lattice_ab_group_add
+    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
+    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
+    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
+    lordered_ring                       ~> lattice_ring
+
 INCOMPATIBILITY.
 
 * Index syntax for structures must be imported explicitly from library