# HG changeset patch
# User wenzelm
# Date 939130346 -7200
# Node ID 7f073ed51193c89dafdb01b3fcb8e5e2c4063e4c
# Parent  8add8fdce3f1f6740492c5245adfd1d7a7bb458f
added Thy/latex.ML;
removed Thy/browser_info.ML;
use "../Isar/outer_lex.ML";

diff -r 8add8fdce3f1 -r 7f073ed51193 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";