equal
deleted
inserted
replaced
15 Readthy.loaded_thys := !loaded_thys; |
15 Readthy.loaded_thys := !loaded_thys; |
16 open Readthy; |
16 open Readthy; |
17 |
17 |
18 use_thy "Holcfb"; |
18 use_thy "Holcfb"; |
19 use_thy "Void"; |
19 use_thy "Void"; |
|
20 |
|
21 use_thy "Porder0"; |
20 use_thy "Porder"; |
22 use_thy "Porder"; |
|
23 |
21 use_thy "Pcpo"; |
24 use_thy "Pcpo"; |
22 |
25 |
23 use_thy "Fun1"; |
26 use_thy "Fun1"; |
24 use_thy "Fun2"; |
27 use_thy "Fun2"; |
25 use_thy "Fun3"; |
28 use_thy "Fun3"; |
59 |
62 |
60 use_thy "Dnat"; |
63 use_thy "Dnat"; |
61 use_thy "Dnat2"; |
64 use_thy "Dnat2"; |
62 use_thy "Stream"; |
65 use_thy "Stream"; |
63 use_thy "Stream2"; |
66 use_thy "Stream2"; |
|
67 use_thy "Dlist"; |
|
68 |
64 |
69 |
65 use "../Pure/install_pp.ML"; |
70 use "../Pure/install_pp.ML"; |
66 print_depth 8; |
71 print_depth 8; |
67 |
72 |
68 val HOLCF_build_completed = (); (*indicate successful build*) |
73 val HOLCF_build_completed = (); (*indicate successful build*) |