author | wenzelm |
Fri, 05 Feb 1999 21:02:17 +0100 | |
changeset 6242 | 3d75f5a99f60 |
parent 6241 | d3c6184ca6c5 |
child 6243 | fb293dfa2df3 |
--- a/src/Pure/Isar/ROOT.ML Fri Feb 05 21:01:53 1999 +0100 +++ b/src/Pure/Isar/ROOT.ML Fri Feb 05 21:02:17 1999 +0100 @@ -20,14 +20,16 @@ (*interactive subsystem*) use "proof_history.ML"; use "toplevel.ML"; -use "outer_syntax.ML"; -(*theory operations and syntax*) +(*theory operations*) use "isar_thy.ML"; use "isar_cmd.ML"; + +(*theory syntax*) +use "outer_syntax.ML"; use "isar_syn.ML"; -(*main interface*) +(*main ML interface*) use "isar.ML"; structure PureIsar =