equal
deleted
inserted
replaced
57 use_thy "Sexp"; |
57 use_thy "Sexp"; |
58 use_thy "WF_Rel"; |
58 use_thy "WF_Rel"; |
59 use_thy "Map"; |
59 use_thy "Map"; |
60 use_thy "Update"; |
60 use_thy "Update"; |
61 |
61 |
|
62 use_dir "Integ"; |
|
63 |
62 (*TFL: recursive function definitions*) |
64 (*TFL: recursive function definitions*) |
63 cd "$ISABELLE_HOME/src/TFL"; |
65 cd "$ISABELLE_HOME/src/TFL"; |
64 use "sys.sml"; |
66 use "sys.sml"; |
|
67 cd "$ISABELLE_HOME/src/HOL"; |
65 |
68 |
66 print_depth 8; |
69 print_depth 8; |
67 |
70 |
68 val HOL_build_completed = (); (*indicate successful build*) |
71 val HOL_build_completed = (); (*indicate successful build*) |