# HG changeset patch
# User bulwahn
# Date 1311583352 -7200
# Node ID 64f88ef1835e125c86c86d056ee679f694a1c6e1
# Parent  4611af362cd03c8101c01039ab8c9e3c9f010e88
NEWS

diff -r 4611af362cd0 -r 64f88ef1835e NEWS
--- 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.