added html.ML, browser_info.ML;
authorwenzelm
Tue Mar 09 12:12:02 1999 +0100 (1999-03-09)
changeset 6323e5b3e46d5dbd
parent 6322 7047300264c9
child 6324 3b7111b360b1
added html.ML, browser_info.ML;
src/Pure/Thy/ROOT.ML
     1.1 --- a/src/Pure/Thy/ROOT.ML	Tue Mar 09 12:11:29 1999 +0100
     1.2 +++ b/src/Pure/Thy/ROOT.ML	Tue Mar 09 12:12:02 1999 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  use "thy_info.ML";
     1.5  
     1.6  (*theory presentation*)
     1.7 -(*use "html.ML";*)
     1.8 -(*use "browser_info.ML";*)	(* FIXME *)
     1.9 +use "html.ML";
    1.10 +use "browser_info.ML";
    1.11  use "present.ML";
    1.12  use "thm_database.ML";
    1.13