tuned
authorhaftmann
Wed May 30 21:09:09 2007 +0200 (2007-05-30)
changeset 23129a318773dca05
parent 23128 8e0abe0fa80f
child 23130 cf50eb79d107
tuned
NEWS
     1.1 --- a/NEWS	Wed May 30 18:05:10 2007 +0200
     1.2 +++ b/NEWS	Wed May 30 21:09:09 2007 +0200
     1.3 @@ -542,6 +542,13 @@
     1.4      Nat.power ~> Nat.power_class.power
     1.5      Nat.size ~> Nat.size_class.size
     1.6      Numeral.number_of ~> Numeral.number_class.number_of
     1.7 +    FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf
     1.8 +
     1.9 +* Rudimentary class target mechanims involves constant renames:
    1.10 +
    1.11 +    Orderings.min ~> Orderings.ord_class.min
    1.12 +    Orderings.max ~> Orderings.ord_class.max
    1.13 +    FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
    1.14  
    1.15  * case expressions and primrec: missing cases now mapped to "undefined"
    1.16  instead of "arbitrary"
    1.17 @@ -578,7 +585,7 @@
    1.18      Instantiation of lattice classes allows explicit definitions
    1.19      for "inf" and "sup" operations.
    1.20  
    1.21 -  INCOMPATIBILITY. Theorem renames:
    1.22 +  INCOMPATIBILITY.  Theorem renames:
    1.23  
    1.24      meet_left_le            ~> inf_le1
    1.25      meet_right_le           ~> inf_le2