equal
deleted
inserted
replaced
9 |
9 |
10 val _ = |
10 val _ = |
11 Outer_Syntax.command |
11 Outer_Syntax.command |
12 (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory" |
12 (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory" |
13 (Thy_Header.args >> (fn header => |
13 (Thy_Header.args >> (fn header => |
14 Toplevel.print o |
14 Toplevel.init_theory |
15 Toplevel.init_theory |
15 (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header))); |
16 (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header))); |
|
17 |
16 |
18 val _ = |
17 val _ = |
19 Outer_Syntax.command |
18 Outer_Syntax.command |
20 (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" |
19 (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" |
21 (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |
20 (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |