NEWS
changeset 22997 d4f3b015b50b
parent 22972 3e96b98d37c6
child 23013 c38c9039dc13
     1.1 --- a/NEWS	Thu May 17 19:49:21 2007 +0200
     1.2 +++ b/NEWS	Thu May 17 19:49:40 2007 +0200
     1.3 @@ -530,6 +530,15 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Constant renames due to introduction of canonical name prefixing for
     1.8 +  class package:
     1.9 +
    1.10 +    HOL.abs ~> HOL.minus_class.abs
    1.11 +    HOL.divide ~> HOL.divide_class.divide
    1.12 +    Nat.power ~> Nat.power_class.power
    1.13 +    Nat.size ~> Nat.size_class.size
    1.14 +    Numeral.number_of ~> Numeral.number_class.number_of
    1.15 +
    1.16  * case expressions and primrec: missing cases now mapped to "undefined"
    1.17  instead of "arbitrary"
    1.18  
    1.19 @@ -675,7 +684,7 @@
    1.20  type "'a::size ==> bool"
    1.21  
    1.22  * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
    1.23 -dvd" to "Divides.div", "Divides.mod" and "Divides.dvd". INCOMPATIBILITY.
    1.24 +dvd" to "Divides.div_class.div", "Divides.div_class.mod" and "Divides.dvd". INCOMPATIBILITY.
    1.25  
    1.26  * Added method "lexicographic_order" automatically synthesizes
    1.27  termination relations as lexicographic combinations of size measures
    1.28 @@ -708,7 +717,7 @@
    1.29  rarely occuring name references (e.g. ``List.op mem.simps'') require
    1.30  renaming (e.g. ``List.memberl.simps'').
    1.31  
    1.32 -* Renamed constants "0" to "HOL.zero" and "1" to "HOL.one".
    1.33 +* Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one".
    1.34  INCOMPATIBILITY.
    1.35  
    1.36  * Added theory Code_Generator providing class 'eq', allowing for code
    1.37 @@ -737,12 +746,12 @@
    1.38  "A = B" (with priority 50).
    1.39  
    1.40  * Renamed constants in HOL.thy and Orderings.thy:
    1.41 -    op +   ~> HOL.plus
    1.42 -    op -   ~> HOL.minus
    1.43 -    uminus ~> HOL.uminus
    1.44 -    op *   ~> HOL.times
    1.45 -    op <   ~> Orderings.less
    1.46 -    op <=  ~> Orderings.less_eq
    1.47 +    op +   ~> HOL.plus_class.plus
    1.48 +    op -   ~> HOL.minus_class.minus
    1.49 +    uminus ~> HOL.minus_class.uminus
    1.50 +    op *   ~> HOL.times_class.times
    1.51 +    op <   ~> Orderings.ord_class.less
    1.52 +    op <=  ~> Orderings.ord_class.less_eq
    1.53  
    1.54  Adaptions may be required in the following cases:
    1.55  
    1.56 @@ -763,7 +772,8 @@
    1.57  
    1.58  d) ML code directly refering to constant names
    1.59  This in general only affects hand-written proof tactics, simprocs and so on.
    1.60 -INCOMPATIBILITY: grep your sourcecode and replace names.
    1.61 +INCOMPATIBILITY: grep your sourcecode and replace names.  Consider use
    1.62 +of const_name ML antiquotations.
    1.63  
    1.64  * Relations less (<) and less_eq (<=) are also available on type bool.
    1.65  Modified syntax to disallow nesting without explicit parentheses,