--- a/NEWS Wed Jul 30 16:07:00 2008 +0200
+++ b/NEWS Wed Jul 30 19:03:33 2008 +0200
@@ -125,6 +125,13 @@
*** HOL-Algebra ***
+* New locales for orders and lattices where the equivalence relation
+ is not restricted to equality. INCOMPATIBILITY: all order and
+ lattice locales use a record structure with field eq for the
+ equivalence.
+
+* New theory of factorial domains.
+
* Units_l_inv and Units_r_inv are now simprules by default.
INCOMPATIBILITY. Simplifier proof that require deletion of l_inv
and/or r_inv will now also require deletion of these lemmas.
@@ -136,8 +143,6 @@
greatest_carrier ~> greatest_closed
greatest_Lower_above ~> greatest_Lower_below
-* New theory of factorial domains.
-
*** HOL-NSA ***