equal
deleted
inserted
replaced
55 use_thy "WF_Rel"; |
55 use_thy "WF_Rel"; |
56 use_thy "List"; |
56 use_thy "List"; |
57 use_thy "Map"; |
57 use_thy "Map"; |
58 |
58 |
59 (*TFL: recursive function definitions*) |
59 (*TFL: recursive function definitions*) |
60 cd "../TFL"; |
60 cd "$ISABELLE_HOME/src/TFL"; |
61 use "sys.sml"; |
61 use "sys.sml"; |
62 cd "../HOL"; |
|
63 |
62 |
64 print_depth 8; |
63 print_depth 8; |
65 |
64 |
66 val HOL_build_completed = (); (*indicate successful build*) |
65 val HOL_build_completed = (); (*indicate successful build*) |