equal
deleted
inserted
replaced
120 the "isabelle-export:" file-system. To get generated code dumped into |
120 the "isabelle-export:" file-system. To get generated code dumped into |
121 output, use "file \<open>\<close>". Minor INCOMPATIBILITY. |
121 output, use "file \<open>\<close>". Minor INCOMPATIBILITY. |
122 |
122 |
123 * Code generation for OCaml: proper strings are used for literals. |
123 * Code generation for OCaml: proper strings are used for literals. |
124 Minor INCOMPATIBILITY. |
124 Minor INCOMPATIBILITY. |
|
125 |
|
126 * Code generation for OCaml: Zarith superseedes Nums as library for |
|
127 integer arithmetic. Use the following incantation to obtain a suitable |
|
128 component setup: |
|
129 |
|
130 isabelle ocaml_setup |
|
131 isabelle ocaml_opam install zarith |
|
132 |
|
133 Minor INCOMPATIBILITY |
125 |
134 |
126 * Code generation for Haskell: code includes for Haskell must contain |
135 * Code generation for Haskell: code includes for Haskell must contain |
127 proper module frame, nothing is added magically any longer. |
136 proper module frame, nothing is added magically any longer. |
128 INCOMPATIBILITY. |
137 INCOMPATIBILITY. |
129 |
138 |