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;