improved load paths;
authorwenzelm
Thu Apr 22 18:25:07 1999 +0200 (1999-04-22)
changeset 64904961ecbaaff7
parent 6489 e02c5290885d
child 6491 7954ffeb93f3
improved load paths;
src/HOL/Lambda/ROOT.ML
src/HOL/Real/ROOT.ML
     1.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Apr 22 18:23:45 1999 +0200
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Thu Apr 22 18:25:07 1999 +0200
     1.3 @@ -7,5 +7,5 @@
     1.4  writeln"Root file for HOL/Lambda";
     1.5  
     1.6  time_use_thy "Eta";
     1.7 -add_path "../Induct";
     1.8 +time_use_thy "../Induct/Acc";
     1.9  time_use_thy "InductTermi";
     2.1 --- a/src/HOL/Real/ROOT.ML	Thu Apr 22 18:23:45 1999 +0200
     2.2 +++ b/src/HOL/Real/ROOT.ML	Thu Apr 22 18:25:07 1999 +0200
     2.3 @@ -10,9 +10,7 @@
     2.4  
     2.5  set proof_timing;
     2.6  time_use_thy "RealDef";
     2.7 -use          "simproc";
     2.8 +use          "simproc.ML";
     2.9  time_use_thy "RealAbs";
    2.10  time_use_thy "RComplete";
    2.11 -
    2.12 -add_path "Hyperreal";
    2.13 -use_thy "Filter";
    2.14 +time_use_thy "Hyperreal/Filter";