changeset 7728 | 2e737ce3cdb5 |
parent 7680 | 27bbbe36d49a |
child 8091 | 226dcdc3c5f3 |
7727:b52c7d773121 | 7728:2e737ce3cdb5 |
---|---|
21 use "skip_proof.ML"; |
21 use "skip_proof.ML"; |
22 use "obtain.ML"; |
22 use "obtain.ML"; |
23 |
23 |
24 (*outer syntax*) |
24 (*outer syntax*) |
25 use "comment.ML"; |
25 use "comment.ML"; |
26 use "outer_lex.ML"; |
26 (*use "outer_lex.ML";*) (*see ../Thy/ROOT.ML*) |
27 use "outer_parse.ML"; |
27 use "outer_parse.ML"; |
28 |
28 |
29 (*toplevel environment*) |
29 (*toplevel environment*) |
30 use "toplevel.ML"; |
30 use "toplevel.ML"; |
31 use "session.ML"; |
31 use "session.ML"; |