--- a/src/Pure/IsaMakefile Tue Aug 16 13:42:26 2005 +0200
+++ b/src/Pure/IsaMakefile Tue Aug 16 13:42:29 2005 +0200
@@ -38,11 +38,11 @@
Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML \
Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML Isar/method.ML \
Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
- Isar/proof.ML Isar/proof_context.ML Isar/proof_history.ML \
- Isar/rule_cases.ML Isar/session.ML Isar/skip_proof.ML \
- Isar/term_style.ML Isar/thy_header.ML Isar/toplevel.ML \
- ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \
+ Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
+ Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_history.ML Isar/rule_cases.ML Isar/session.ML \
+ Isar/skip_proof.ML Isar/term_style.ML Isar/thy_header.ML \
+ Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \
ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML \
ML-Systems/polyml-posix.ML ML-Systems/smlnj-basis-compat.ML \
ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-ptreql.ML \
--- a/src/Pure/Isar/ROOT.ML Tue Aug 16 13:42:26 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML Tue Aug 16 13:42:29 2005 +0200
@@ -15,10 +15,10 @@
use "attrib.ML";
use "locale.ML";
use "proof.ML";
+use "method.ML";
use "proof_history.ML";
use "net_rules.ML";
use "induct_attrib.ML";
-use "method.ML";
(*derived proof elements*)
use "calculation.ML";
@@ -28,15 +28,18 @@
(*outer syntax*)
use "antiquote.ML";
use "outer_parse.ML";
+use "outer_keyword.ML";
(*toplevel environment*)
use "toplevel.ML";
+
+(*theory presentation*)
use "term_style.ML";
use "isar_output.ML";
-use "session.ML";
(*theory syntax*)
use "thy_header.ML";
+use "session.ML";
use "outer_syntax.ML";
(*theory and proof operations*)