globbing constant expressions use more idiomatic underscore rather than star;
authorhaftmann
Fri Nov 26 12:03:17 2010 +0100 (2010-11-26)
changeset 40710499aa989fbad
parent 40709 b29c70cd5c93
child 40711 81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star;
precised
NEWS
     1.1 --- a/NEWS	Fri Nov 26 11:38:20 2010 +0100
     1.2 +++ b/NEWS	Fri Nov 26 12:03:17 2010 +0100
     1.3 @@ -89,6 +89,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generator: globbing constant expressions "*" and "Theory.*" have been
     1.8 +replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
     1.9 +
    1.10  * Theory Enum (for explicit enumerations of finite types) is now part of
    1.11  the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now 
    1.12  have to be referred to by its qualified name.
    1.13 @@ -101,7 +104,7 @@
    1.14  avoid confusion with finite sets.  INCOMPATIBILITY.
    1.15  
    1.16  * Quickcheck's generator for random generation is renamed from "code" to
    1.17 -"random". INCOMPATIBILITY. 
    1.18 +"random".  INCOMPATIBILITY. 
    1.19  
    1.20  * Theory Multiset provides stable quicksort implementation of sort_key.
    1.21  
    1.22 @@ -124,7 +127,7 @@
    1.23  * Constant `contents` renamed to `the_elem`, to free the generic name
    1.24  contents for other uses.  INCOMPATIBILITY.
    1.25  
    1.26 -* Dropped old primrec package.  INCOMPATIBILITY.
    1.27 +* Dropped syntax for old primrec package.  INCOMPATIBILITY.
    1.28  
    1.29  * Improved infrastructure for term evaluation using code generator
    1.30  techniques, in particular static evaluation conversions.