| changeset 80 | 95e9c4556221 |
| parent 64 | 9a6e5e0c4906 |
| child 106 | bdd82350cf22 |
| 79:a53c7810e38b | 80:95e9c4556221 |
|---|---|
13 (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl) |
13 (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl) |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
16 *} |
16 *} |
17 |
17 |
18 |
|
18 end |
19 end |