# HG changeset patch
# User haftmann
# Date 1193405822 -7200
# Node ID e83c6c43f1e6745f25425ee17db9996ce2e120d4
# Parent  1e904070e9cbf42c53c84d5af977f7572cad57d2
tuned

diff -r 1e904070e9cb -r e83c6c43f1e6 NEWS
--- a/NEWS	Fri Oct 26 14:24:32 2007 +0200
+++ b/NEWS	Fri Oct 26 15:37:02 2007 +0200
@@ -120,20 +120,20 @@
 See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).
 "isatool doc classes" provides a tutorial.
 
-* Yet another code generator framework allows to generate executable
+* Generic code generator framework allows to generate executable
 code for ML and Haskell (including Isabelle classes).  A short usage
 sketch:
 
     internal compilation:
-        code_gen <list of constants (term syntax)> in SML
+        export_code <list of constants (term syntax)> in SML
     writing SML code to a file:
-        code_gen <list of constants (term syntax)> in SML <filename>
+        export_code <list of constants (term syntax)> in SML <filename>
     writing OCaml code to a file:
-        code_gen <list of constants (term syntax)> in OCaml <filename>
+        export_code <list of constants (term syntax)> in OCaml <filename>
     writing Haskell code to a bunch of files:
-        code_gen <list of constants (term syntax)> in Haskell <filename>
-
-    evaluating propositions to True/False using code generation:
+        export_code <list of constants (term syntax)> in Haskell <filename>
+
+    evaluating closed propositions to True/False using code generation:
         method ``eval''
 
 Reasonable default setup of framework in HOL.
@@ -161,7 +161,7 @@
       {(target) <and-list of class target syntax>}+
         where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
 
-code_instance and code_class only apply to target Haskell.
+code_instance and code_class only are effective to target Haskell.
 
 For example usage see src/HOL/ex/Codegenerator.thy and
 src/HOL/ex/Codegenerator_Pretty.thy.  A separate tutorial on code