| changeset 20207 | 4c57e850e8d5 |
| parent 20075 | a7e183bfebef |
| child 20225 | 4b8e42490e58 |
| 20206:eb529c6883ec | 20207:4c57e850e8d5 |
|---|---|
69 (*theory syntax*) |
69 (*theory syntax*) |
70 use "Isar/outer_lex.ML"; |
70 use "Isar/outer_lex.ML"; |
71 |
71 |
72 (*the Isar system*) |
72 (*the Isar system*) |
73 cd "Isar"; use "ROOT.ML"; cd ".."; |
73 cd "Isar"; use "ROOT.ML"; cd ".."; |
74 use "subgoal.ML"; |
|
74 |
75 |
75 use "Proof/extraction.ML"; |
76 use "Proof/extraction.ML"; |
76 |
77 |
77 cd "Tools"; use "ROOT.ML"; cd ".."; |
78 cd "Tools"; use "ROOT.ML"; cd ".."; |
78 |
79 |