# HG changeset patch
# User wenzelm
# Date 1114278520 -7200
# Node ID 0201d0634f8d322799a98e428ba63753afde6fc2
# Parent  5ff7d5d2e0836035286be69f473b99dac9ebc003
content moved to Pure/ROOT.ML;

diff -r 5ff7d5d2e083 -r 0201d0634f8d src/Pure/Proof/ROOT.ML
--- a/src/Pure/Proof/ROOT.ML	Sat Apr 23 19:48:15 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      Pure/Proof/ROOT.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
-
-Proof term operations.
-*)
-
-use "reconstruct.ML";
-use "proof_syntax.ML";
-use "proof_rewrite_rules.ML";
-use "proofchecker.ML";
diff -r 5ff7d5d2e083 -r 0201d0634f8d src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Sat Apr 23 19:48:15 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      Pure/Thy/ROOT.ML
-    ID:         $Id$
-
-Theory system operations.
-*)
-
-(*theory auto loader database*)
-use "thy_load.ML";
-use "thy_info.ML";
-
-(*theory syntax -- old format*)
-use "thy_scan.ML";
-use "thy_parse.ML";
-use "thy_syn.ML";
-
-(*theory syntax -- new format*)
-use "../Isar/outer_lex.ML";
-
-(*theory presentation*)
-use "html.ML";
-use "latex.ML";
-use "present.ML";
-use "thm_deps.ML";
-
-(*theorem database interface*)
-use "thm_database.ML";