changeset 1297 | 7ac266cf82d0 |
parent 393 | 02b27671b899 |
child 1361 | 90d615b599d9 |
1296:ae31bb7774a7 | 1297:7ac266cf82d0 |
---|---|
17 use_thy "LK"; |
17 use_thy "LK"; |
18 |
18 |
19 use "../Pure/install_pp.ML"; |
19 use "../Pure/install_pp.ML"; |
20 print_depth 8; |
20 print_depth 8; |
21 |
21 |
22 make_chart (); (*make HTML chart*) |
|
23 |
|
22 val LK_build_completed = (); (*indicate successful build*) |
24 val LK_build_completed = (); (*indicate successful build*) |