equal
deleted
inserted
replaced
80 * Code generation: command 'export_code' without file keyword exports |
80 * Code generation: command 'export_code' without file keyword exports |
81 code as regular theory export, which can be materialized using the |
81 code as regular theory export, which can be materialized using the |
82 command-line tool "isabelle export" or 'export_files' in the session |
82 command-line tool "isabelle export" or 'export_files' in the session |
83 ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:" |
83 ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:" |
84 file-system. To get generated code dumped into output, use "file \<open>\<close>". |
84 file-system. To get generated code dumped into output, use "file \<open>\<close>". |
|
85 Minor INCOMPATIBILITY. |
|
86 |
|
87 * Code generation for OCaml: proper strings are used for literals. |
85 Minor INCOMPATIBILITY. |
88 Minor INCOMPATIBILITY. |
86 |
89 |
87 * Code generation for Haskell: code includes for Haskell must contain |
90 * Code generation for Haskell: code includes for Haskell must contain |
88 proper module frame, nothing is added magically any longer. |
91 proper module frame, nothing is added magically any longer. |
89 INCOMPATIBILITY. |
92 INCOMPATIBILITY. |