src/HOL/ROOT.ML
changeset 5078 7b5ea59c0275
parent 4896 4727272f3db6
child 5097 6c4a7ad6ebc7
     1.1 --- a/src/HOL/ROOT.ML	Wed Jun 24 13:59:45 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Thu Jun 25 13:57:34 1998 +0200
     1.3 @@ -59,9 +59,12 @@
     1.4  use_thy "Map";
     1.5  use_thy "Update";
     1.6  
     1.7 +use_dir "Integ";
     1.8 +
     1.9  (*TFL: recursive function definitions*)
    1.10  cd "$ISABELLE_HOME/src/TFL";
    1.11  use "sys.sml";
    1.12 +cd "$ISABELLE_HOME/src/HOL";
    1.13  
    1.14  print_depth 8;
    1.15