--- a/NEWS Wed Feb 10 08:49:26 2010 +0100
+++ b/NEWS Wed Feb 10 08:49:26 2010 +0100
@@ -20,6 +20,15 @@
consistent names suitable for name prefixes within the HOL theories.
INCOMPATIBILITY.
+* Some generic constants have been put to appropriate theories:
+
+ inverse, divide: Rings
+
+INCOMPATIBILITY.
+
+* Class division ring also requires proof of fact divide_inverse. However instantiation
+of parameter divide has also been required previously. INCOMPATIBILITY.
+
* More consistent naming of type classes involving orderings (and lattices):
lower_semilattice ~> semilattice_inf
@@ -76,7 +85,7 @@
* New theory Algebras contains generic algebraic structures and
generic algebraic operations. INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and
+plus, minus, uminus, times, abs, sgn, less_eq and
less have been moved from HOL.thy to Algebras.thy.
* HOLogic.strip_psplit: types are returned in syntactic order, similar