tuned
authorhaftmann
Fri, 26 Oct 2007 15:37:02 +0200
changeset 25199e83c6c43f1e6
parent 25198 1e904070e9cb
child 25200 f1d2e106f2fe
tuned
NEWS
     1.1 --- a/NEWS	Fri Oct 26 14:24:32 2007 +0200
     1.2 +++ b/NEWS	Fri Oct 26 15:37:02 2007 +0200
     1.3 @@ -120,20 +120,20 @@
     1.4  See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).
     1.5  "isatool doc classes" provides a tutorial.
     1.6  
     1.7 -* Yet another code generator framework allows to generate executable
     1.8 +* Generic code generator framework allows to generate executable
     1.9  code for ML and Haskell (including Isabelle classes).  A short usage
    1.10  sketch:
    1.11  
    1.12      internal compilation:
    1.13 -        code_gen <list of constants (term syntax)> in SML
    1.14 +        export_code <list of constants (term syntax)> in SML
    1.15      writing SML code to a file:
    1.16 -        code_gen <list of constants (term syntax)> in SML <filename>
    1.17 +        export_code <list of constants (term syntax)> in SML <filename>
    1.18      writing OCaml code to a file:
    1.19 -        code_gen <list of constants (term syntax)> in OCaml <filename>
    1.20 +        export_code <list of constants (term syntax)> in OCaml <filename>
    1.21      writing Haskell code to a bunch of files:
    1.22 -        code_gen <list of constants (term syntax)> in Haskell <filename>
    1.23 -
    1.24 -    evaluating propositions to True/False using code generation:
    1.25 +        export_code <list of constants (term syntax)> in Haskell <filename>
    1.26 +
    1.27 +    evaluating closed propositions to True/False using code generation:
    1.28          method ``eval''
    1.29  
    1.30  Reasonable default setup of framework in HOL.
    1.31 @@ -161,7 +161,7 @@
    1.32        {(target) <and-list of class target syntax>}+
    1.33          where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
    1.34  
    1.35 -code_instance and code_class only apply to target Haskell.
    1.36 +code_instance and code_class only are effective to target Haskell.
    1.37  
    1.38  For example usage see src/HOL/ex/Codegenerator.thy and
    1.39  src/HOL/ex/Codegenerator_Pretty.thy.  A separate tutorial on code