globbing constant expressions use more idiomatic underscore rather than star;
authorhaftmann
Fri, 26 Nov 2010 12:03:17 +0100
changeset 40710 499aa989fbad
parent 40709 b29c70cd5c93
child 40711 81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star; precised
NEWS
--- a/NEWS	Fri Nov 26 11:38:20 2010 +0100
+++ b/NEWS	Fri Nov 26 12:03:17 2010 +0100
@@ -89,6 +89,9 @@
 
 *** HOL ***
 
+* Code generator: globbing constant expressions "*" and "Theory.*" have been
+replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
+
 * Theory Enum (for explicit enumerations of finite types) is now part of
 the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now 
 have to be referred to by its qualified name.
@@ -101,7 +104,7 @@
 avoid confusion with finite sets.  INCOMPATIBILITY.
 
 * Quickcheck's generator for random generation is renamed from "code" to
-"random". INCOMPATIBILITY. 
+"random".  INCOMPATIBILITY. 
 
 * Theory Multiset provides stable quicksort implementation of sort_key.
 
@@ -124,7 +127,7 @@
 * Constant `contents` renamed to `the_elem`, to free the generic name
 contents for other uses.  INCOMPATIBILITY.
 
-* Dropped old primrec package.  INCOMPATIBILITY.
+* Dropped syntax for old primrec package.  INCOMPATIBILITY.
 
 * Improved infrastructure for term evaluation using code generator
 techniques, in particular static evaluation conversions.