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