--- a/NEWS Wed Feb 10 14:12:04 2010 +0100
+++ b/NEWS Wed Feb 10 14:12:30 2010 +0100
@@ -22,6 +22,8 @@
* Some generic constants have been put to appropriate theories:
+ less_eq, less: Orderings
+ abs, sgn: Groups
inverse, divide: Rings
INCOMPATIBILITY.
@@ -80,13 +82,9 @@
INCOMPATIBILITY.
-* Index syntax for structures must be imported explicitly from library
-theory Structure_Syntax. INCOMPATIBILITY.
-
* New theory Algebras contains generic algebraic structures and
generic algebraic operations. INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus, times, abs, sgn, less_eq and
-less have been moved from HOL.thy to Algebras.thy.
+plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.