changeset 1294 | 1358dc040edb |
parent 393 | 02b27671b899 |
child 1361 | 90d615b599d9 |
1293:4ade5d1d369c | 1294:1358dc040edb |
---|---|
21 use_thy "Bool"; |
21 use_thy "Bool"; |
22 |
22 |
23 use "../Pure/install_pp.ML"; |
23 use "../Pure/install_pp.ML"; |
24 print_depth 8; |
24 print_depth 8; |
25 |
25 |
26 make_chart (); (*make HTML chart*) |
|
27 |
|
26 val CTT_build_completed = (); (*indicate successful build*) |
28 val CTT_build_completed = (); (*indicate successful build*) |