# HG changeset patch
# User wenzelm
# Date 920977922 -3600
# Node ID e5b3e46d5dbdcf1c267c8d05df8ca32ce1e1809c
# Parent  7047300264c9c29ef19b5ece1f78722a9d9a283b
added html.ML, browser_info.ML;

diff -r 7047300264c9 -r e5b3e46d5dbd src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Tue Mar 09 12:11:29 1999 +0100
+++ b/src/Pure/Thy/ROOT.ML	Tue Mar 09 12:12:02 1999 +0100
@@ -9,8 +9,8 @@
 use "thy_info.ML";
 
 (*theory presentation*)
-(*use "html.ML";*)
-(*use "browser_info.ML";*)	(* FIXME *)
+use "html.ML";
+use "browser_info.ML";
 use "present.ML";
 use "thm_database.ML";