src/HOL/ROOT.ML
changeset 5107 2edf5dfb02f3
parent 5105 0ff5bec04d02
child 5110 2497807020fa
     1.1 --- a/src/HOL/ROOT.ML	Wed Jul 01 17:59:25 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Wed Jul 01 18:43:40 1998 +0200
     1.3 @@ -56,7 +56,9 @@
     1.4  use_thy "Map";
     1.5  use_thy "Update";
     1.6  
     1.7 -use_dir "Integ";
     1.8 +cd "Integ";
     1.9 +use "ROOT.ML";
    1.10 +cd "..";
    1.11  
    1.12  (*TFL: recursive function definitions*)
    1.13  cd "$ISABELLE_HOME/src/TFL";