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.