NEWS
changeset 23881 851c74f1bb69
parent 23850 f1434532a562
child 23888 babe337cce2d
     1.1 --- a/NEWS	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/NEWS	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -943,9 +943,10 @@
     1.4      op +   ~> HOL.plus_class.plus
     1.5      op -   ~> HOL.minus_class.minus
     1.6      uminus ~> HOL.minus_class.uminus
     1.7 +    abs    ~> HOL.abs_class.abs
     1.8      op *   ~> HOL.times_class.times
     1.9 -    op <   ~> Orderings.ord_class.less
    1.10 -    op <=  ~> Orderings.ord_class.less_eq
    1.11 +    op <   ~> HOL.ord_class.less
    1.12 +    op <=  ~> HOL.ord_class.less_eq
    1.13  
    1.14  Adaptions may be required in the following cases:
    1.15  
    1.16 @@ -1044,7 +1045,7 @@
    1.17  r and finally gets the theorem t = r, which is again applied to the
    1.18  subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
    1.19  
    1.20 -* Reflection: Automatic refification now handels binding, an example
    1.21 +* Reflection: Automatic reification now handels binding, an example
    1.22  is available in HOL/ex/ReflectionEx.thy
    1.23  
    1.24