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