--- a/NEWS Fri Feb 19 11:06:22 2010 +0100
+++ b/NEWS Fri Feb 19 14:46:59 2010 +0100
@@ -28,7 +28,7 @@
* Some generic constants have been put to appropriate theories:
less_eq, less: Orderings
- abs, sgn: Groups
+ zero, one, plus, minus, uminus, times, abs, sgn: Groups
inverse, divide: Rings
INCOMPATIBILITY.
@@ -88,8 +88,7 @@
INCOMPATIBILITY.
* New theory Algebras contains generic algebraic structures and
-generic algebraic operations. INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
+generic algebraic operations.
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.