# HG changeset patch
# User wenzelm
# Date 924798307 -7200
# Node ID 4961ecbaaff7623a35a75d46ab83d55c40fe847b
# Parent  e02c5290885d7450d5a833ac19427a8c3bd04358
improved load paths;

diff -r e02c5290885d -r 4961ecbaaff7 src/HOL/Lambda/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";
diff -r e02c5290885d -r 4961ecbaaff7 src/HOL/Real/ROOT.ML
--- 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";