# HG changeset patch
# User wenzelm
# Date 1144601476 -7200
# Node ID 44937faf9e1a0d4ce122846641d82c2a34e2d14f
# Parent  6cd8abc7f15b6a58f9ad27caf0f4ea6a70ab8e37
moved theory presentation to Isar/ROOT.ML;

diff -r 6cd8abc7f15b -r 44937faf9e1a src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sun Apr 09 18:51:15 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sun Apr 09 18:51:16 2006 +0200
@@ -5,13 +5,22 @@
 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
 *)
 
-(*basic proof engine*)
+(*proof context*)
 use "object_logic.ML";
 use "rule_cases.ML";
 use "auto_bind.ML";
 use "local_syntax.ML";
 use "proof_context.ML";
 use "local_defs.ML";
+
+(*theory presentation*)
+use "../Thy/html.ML";
+use "../Thy/latex.ML";
+use "../Thy/present.ML";
+use "../Thy/thm_deps.ML";
+use "../Thy/thm_database.ML";
+
+(*basic proof engine*)
 use "proof_display.ML";
 use "args.ML";
 use "attrib.ML";
diff -r 6cd8abc7f15b -r 44937faf9e1a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Apr 09 18:51:15 2006 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 09 18:51:16 2006 +0200
@@ -66,15 +66,6 @@
 (*theory syntax*)
 use "Isar/outer_lex.ML";
 
-(*theory presentation*)
-use "Thy/html.ML";
-use "Thy/latex.ML";
-use "Thy/present.ML";
-use "Thy/thm_deps.ML";
-
-(*theorem database ML interface*)
-use "Thy/thm_database.ML";
-
 (*the Isar system*)
 cd "Isar"; use "ROOT.ML"; cd "..";