# HG changeset patch
# User wenzelm
# Date 1114278589 -7200
# Node ID 1576f9d3ffae5196d57f0866557f1a60980aeee9
# Parent  222eeb9655f3ee6e35c82a0b9740ad9cc646dc9b
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;

diff -r 222eeb9655f3 -r 1576f9d3ffae src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 23 19:49:39 2005 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 23 19:49:49 2005 +0200
@@ -28,7 +28,7 @@
 (*inner syntax module*)
 cd "Syntax"; use "ROOT.ML"; cd "..";
 
-(*core system*)
+(*core of tactical proof system*)
 use "type_infer.ML";
 use "sign.ML";
 use "envir.ML";
@@ -51,10 +51,31 @@
 use "tactic.ML";
 
 (*proof term operations*)
-cd "Proof"; use "ROOT.ML"; cd "..";
+use "Proof/reconstruct.ML";
+use "Proof/proof_syntax.ML";
+use "Proof/proof_rewrite_rules.ML";
+use "Proof/proofchecker.ML";
+
+(*theory auto loader database*)
+use "Thy/thy_load.ML";
+use "Thy/thy_info.ML";
 
-(*theory system operations*)
-cd "Thy"; use "ROOT.ML"; cd "..";
+(*theory syntax -- old format*)
+use "Thy/thy_scan.ML";
+use "Thy/thy_parse.ML";
+use "Thy/thy_syn.ML";
+
+(*theory syntax -- new format*)
+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 subsystem*)
 cd "Isar"; use "ROOT.ML"; cd "..";