changeset 1361 | 90d615b599d9 |
parent 1296 | ae31bb7774a7 |
child 1459 | d12da312eff4 |
1360:6bdee79ef125 | 1361:90d615b599d9 |
---|---|
15 use_thy "Cube"; |
15 use_thy "Cube"; |
16 |
16 |
17 use "../Pure/install_pp.ML"; |
17 use "../Pure/install_pp.ML"; |
18 print_depth 8; |
18 print_depth 8; |
19 |
19 |
20 make_chart (); (*make HTML chart*) |
|
21 |
|
22 val Cube_build_completed = (); (*indicate successful build*) |
20 val Cube_build_completed = (); (*indicate successful build*) |