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