changeset 15434 | cb5bfb32ab39 |
parent 14981 | e73f8140af78 |
child 15452 | e2a721567f67 |
15433:a2cbdf16832e | 15434:cb5bfb32ab39 |
---|---|
31 use "antiquote.ML"; |
31 use "antiquote.ML"; |
32 use "outer_parse.ML"; |
32 use "outer_parse.ML"; |
33 |
33 |
34 (*toplevel environment*) |
34 (*toplevel environment*) |
35 use "toplevel.ML"; |
35 use "toplevel.ML"; |
36 use "isar_output.ML"; |
|
36 use "session.ML"; |
37 use "session.ML"; |
37 use "isar_output.ML"; |
|
38 |
38 |
39 (*theory syntax*) |
39 (*theory syntax*) |
40 use "thy_header.ML"; |
40 use "thy_header.ML"; |
41 use "outer_syntax.ML"; |
41 use "outer_syntax.ML"; |
42 |
42 |