equal
deleted
inserted
replaced
263 allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close> |
263 allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close> |
264 impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close> |
264 impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close> |
265 eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close> |
265 eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close> |
266 \<close> |
266 \<close> |
267 |
267 |
268 The ML function Generate_File.generate writes all generated files from a |
268 See also commands 'export_generated_files' and 'compile_generated_files' |
269 given theory to the file-system, e.g. a temporary directory where some |
269 to use the results. |
270 external compiler is applied. |
|
271 |
270 |
272 * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to |
271 * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to |
273 option ML_environment to select a named environment, such as "Isabelle" |
272 option ML_environment to select a named environment, such as "Isabelle" |
274 for Isabelle/ML, or "SML" for official Standard ML. It is also possible |
273 for Isabelle/ML, or "SML" for official Standard ML. It is also possible |
275 to move toplevel bindings between environments, using a notation with |
274 to move toplevel bindings between environments, using a notation with |