equal
deleted
inserted
replaced
8 struct |
8 struct |
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 >> |
14 Toplevel.init_theory (fn () => Thy_Info.toplevel_begin_theory Path.current header))); |
14 (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
15 |
15 |
16 val _ = |
16 val _ = |
17 Outer_Syntax.command |
17 Outer_Syntax.command |
18 (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" |
18 (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" |
19 (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |
19 (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |