tidied;
authorwenzelm
Wed, 03 Feb 1999 17:29:12 +0100
changeset 6210 465cae203337
parent 6209 7059f46603e2
child 6211 43d0efafa025
tidied;
src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Wed Feb 03 17:28:40 1999 +0100
+++ b/src/Pure/Thy/ROOT.ML	Wed Feb 03 17:29:12 1999 +0100
@@ -1,20 +1,19 @@
 (*  Title:      Pure/Thy/ROOT.ML
     ID:         $Id$
 
-This file builds the theory parser and autoloading system.
+Theory system operations.
 *)
 
-use "use.ML";
+(*theory auto loader database*)
+use "thy_load.ML";
+use "thy_info.ML";
+use "session.ML";
 
+(*theory presentation*)
+use "present.ML";
+use "thm_database.ML";
+
+(*theory syntax (old format)*)  (* FIXME rename to OldThy (!?) *)
 use "thy_scan.ML";
 use "thy_parse.ML";
 use "thy_syn.ML";
-
-use "context.ML";
-
-use "thy_info.ML";
-use "browser_info.ML";
-use "thm_database.ML";
-use "thy_read.ML";
-
-open ThmDatabase ThyRead ThyInfo BrowserInfo;