--- a/NEWS Mon Jul 25 10:40:52 2011 +0200
+++ b/NEWS Mon Jul 25 10:42:32 2011 +0200
@@ -93,7 +93,10 @@
* Code generation:
- theory Library/Code_Char_ord provides native ordering of characters
in the target language.
-
+ - commands code_module and code_library are legacy, use export_code instead.
+ - evaluator "SML" and method evaluation are legacy, use evaluator "code"
+ and method eval instead.
+
* Declare ext [intro] by default. Rare INCOMPATIBILITY.
* Nitpick:
@@ -132,6 +135,8 @@
It requires that the Glasgow Haskell compiler is installed and
its location is known to Isabelle with the environment variable
ISABELLE_GHC.
+ - Removed quickcheck tester "SML" based on the SML code generator
+ from HOL-Library
* Function package: discontinued option "tailrec".
INCOMPATIBILITY. Use partial_function instead.