src/HOL/ROOT.ML
changeset 5110 2497807020fa
parent 5107 2edf5dfb02f3
child 5124 1ce3cccfacdb
     1.1 --- a/src/HOL/ROOT.ML	Wed Jul 01 19:11:20 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Thu Jul 02 16:44:39 1998 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  use_thy "Update";
     1.5  
     1.6  cd "Integ";
     1.7 -use "ROOT.ML";
     1.8 +use_thy "Bin";
     1.9  cd "..";
    1.10  
    1.11  (*TFL: recursive function definitions*)