equal
deleted
inserted
replaced
39 |
39 |
40 use_thy "RelPow"; |
40 use_thy "RelPow"; |
41 use_thy "Finite"; |
41 use_thy "Finite"; |
42 use_thy "Sexp"; |
42 use_thy "Sexp"; |
43 use_thy "Option"; |
43 use_thy "Option"; |
|
44 use_thy "WF_Rel"; |
44 use_thy "List"; |
45 use_thy "List"; |
|
46 |
|
47 (*TFL: recursive function definitions*) |
|
48 cd "../TFL"; |
|
49 use "sys.sml"; |
|
50 cd "../HOL"; |
45 |
51 |
46 init_pps (); |
52 init_pps (); |
47 print_depth 8; |
53 print_depth 8; |
48 |
54 |
49 val HOL_build_completed = (); (*indicate successful build*) |
55 val HOL_build_completed = (); (*indicate successful build*) |