added Thy/latex.ML;
authorwenzelm
Tue, 05 Oct 1999 15:32:26 +0200
changeset 7723 7f073ed51193
parent 7722 8add8fdce3f1
child 7724 280b15f1ae9c
added Thy/latex.ML; removed Thy/browser_info.ML; use "../Isar/outer_lex.ML";
src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Tue Oct 05 15:32:16 1999 +0200
+++ b/src/Pure/Thy/ROOT.ML	Tue Oct 05 15:32:26 1999 +0200
@@ -8,13 +8,17 @@
 use "thy_load.ML";
 use "thy_info.ML";
 
-(*theory presentation*)
-use "html.ML";
-use "browser_info.ML";
-use "present.ML";
-use "thm_database.ML";
-
-(*theory syntax (old format)*)
+(*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_database.ML";