# HG changeset patch
# User ballarin
# Date 1217340896 -7200
# Node ID 15b65db6675165dda5a57fc0f2dc7437367fcedb
# Parent  033732c90ebd4a154ad31bb5fcbba23549431670
Unit_inv_l, Unit_inv_r made [simp];
Renamed theorems;
New theory on divisibility.

diff -r 033732c90ebd -r 15b65db66751 NEWS
--- a/NEWS	Tue Jul 29 14:20:22 2008 +0200
+++ b/NEWS	Tue Jul 29 16:14:56 2008 +0200
@@ -123,6 +123,22 @@
 theorems.  Changes in simp rules.  INCOMPATIBILITY.
 
 
+*** HOL-Algebra ***
+
+* 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