NEWS

 theorems.  Changes in simp rules.  INCOMPATIBILITY.
 
 
 *** 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.
 
 * Renamed the following theorems.  INCOMPATIBILITY.
 UpperD ~> Upper_memD
 LowerD ~> Lower_memD
 least_carrier ~> least_closed
 greatest_carrier ~> greatest_closed
 greatest_Lower_above ~> greatest_Lower_below
-
-* New theory of factorial domains.
 
 
 *** HOL-NSA ***
 
 * Created new image HOL-NSA, containing theories of nonstandard