renamed Isar/isar_output.ML to Thy/thy_output.ML;
authorwenzelm
Fri, 19 Jan 2007 22:08:22 +0100
changeset 22113 4a65d2f4d0b5
parent 22112 6a90ac654c6d
child 22114 560c5b5dda1c
renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML; load outer_parse.ML early, moved later parts to spec_parse.ML; tuned order;
src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Jan 19 22:08:21 2007 +0100
+++ b/src/Pure/Isar/ROOT.ML	Fri Jan 19 22:08:22 2007 +0100
@@ -13,7 +13,17 @@
 use "proof_context.ML";
 use "local_defs.ML";
 
-(*theory presentation*)
+(*outer syntax*)
+use "outer_lex.ML";
+use "args.ML";
+use "outer_parse.ML";
+use "outer_keyword.ML";
+use "antiquote.ML";
+
+(*theory sources*)
+use "../Thy/ml_context.ML";
+use "../Thy/thy_load.ML";
+use "../Thy/thy_info.ML";
 use "../Thy/html.ML";
 use "../Thy/latex.ML";
 use "../Thy/present.ML";
@@ -22,7 +32,6 @@
 
 (*basic proof engine*)
 use "proof_display.ML";
-use "args.ML";
 use "attrib.ML";
 use "context_rules.ML";
 use "skip_proof.ML";
@@ -37,26 +46,22 @@
 use "calculation.ML";
 use "obtain.ML";
 use "locale.ML";
+use "spec_parse.ML";
 use "../axclass.ML";
 use "theory_target.ML";
 use "specification.ML";
 use "constdefs.ML";
 
-(*outer syntax*)
-use "antiquote.ML";
-use "outer_parse.ML";
-use "outer_keyword.ML";
-
 (*toplevel environment*)
 use "proof_history.ML";
 use "toplevel.ML";
 
 (*theory presentation*)
-use "term_style.ML";
-use "isar_output.ML";
+use "../Thy/term_style.ML";
+use "../Thy/thy_output.ML";
 
 (*theory syntax*)
-use "thy_header.ML";
+use "../Thy/thy_header.ML";
 use "session.ML";
 use "../old_goals.ML";
 use "outer_syntax.ML";