1.1 --- a/NEWS	Wed Feb 10 14:12:04 2010 +0100
     1.2 +++ b/NEWS	Wed Feb 10 14:12:30 2010 +0100
     1.3 @@ -22,6 +22,8 @@
     1.4  
     1.5  * Some generic constants have been put to appropriate theories:
     1.6  
     1.7 +    less_eq, less: Orderings
     1.8 +    abs, sgn: Groups
     1.9      inverse, divide: Rings
    1.10  
    1.11  INCOMPATIBILITY.
    1.12 @@ -80,13 +82,9 @@
    1.13  
    1.14  INCOMPATIBILITY.
    1.15  
    1.16 -* Index syntax for structures must be imported explicitly from library
    1.17 -theory Structure_Syntax.  INCOMPATIBILITY.
    1.18 -
    1.19  * New theory Algebras contains generic algebraic structures and
    1.20  generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
    1.21 -plus, minus, uminus, times, abs, sgn, less_eq and
    1.22 -less have been moved from HOL.thy to Algebras.thy.
    1.23 +plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
    1.24  
    1.25  * HOLogic.strip_psplit: types are returned in syntactic order, similar
    1.26  to other strip and tuple operations.  INCOMPATIBILITY.