src/HOL/ROOT.ML
changeset 3195 dcb458d38724
parent 2857 848bce5fe8ad
child 3511 da4dd8b7ced4
--- a/src/HOL/ROOT.ML	Thu May 15 12:53:12 1997 +0200
+++ b/src/HOL/ROOT.ML	Thu May 15 12:53:39 1997 +0200
@@ -41,8 +41,14 @@
 use_thy "Finite";
 use_thy "Sexp";
 use_thy "Option";
+use_thy "WF_Rel";
 use_thy "List";
 
+(*TFL: recursive function definitions*)
+cd "../TFL";
+use "sys.sml";
+cd "../HOL";
+
 init_pps ();
 print_depth 8;