improved load paths;
authorwenzelm
Thu, 22 Apr 1999 18:25:07 +0200
changeset 6490 4961ecbaaff7
parent 6489 e02c5290885d
child 6491 7954ffeb93f3
improved load paths;
src/HOL/Lambda/ROOT.ML
src/HOL/Real/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Thu Apr 22 18:23:45 1999 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Thu Apr 22 18:25:07 1999 +0200
@@ -7,5 +7,5 @@
 writeln"Root file for HOL/Lambda";
 
 time_use_thy "Eta";
-add_path "../Induct";
+time_use_thy "../Induct/Acc";
 time_use_thy "InductTermi";
--- a/src/HOL/Real/ROOT.ML	Thu Apr 22 18:23:45 1999 +0200
+++ b/src/HOL/Real/ROOT.ML	Thu Apr 22 18:25:07 1999 +0200
@@ -10,9 +10,7 @@
 
 set proof_timing;
 time_use_thy "RealDef";
-use          "simproc";
+use          "simproc.ML";
 time_use_thy "RealAbs";
 time_use_thy "RComplete";
-
-add_path "Hyperreal";
-use_thy "Filter";
+time_use_thy "Hyperreal/Filter";