| changeset 1296 | ae31bb7774a7 |
| parent 1008 | fa11e1e28bd3 |
| child 1361 | 90d615b599d9 |
| 1295:27c1e88a62b4 | 1296:ae31bb7774a7 |
|---|---|
76 use "simpdata.ML"; |
76 use "simpdata.ML"; |
77 |
77 |
78 use "../Pure/install_pp.ML"; |
78 use "../Pure/install_pp.ML"; |
79 print_depth 8; |
79 print_depth 8; |
80 |
80 |
81 make_chart (); (*make HTML chart*) |
|
82 |
|
81 val FOLP_build_completed = (); (*indicate successful build*) |
83 val FOLP_build_completed = (); (*indicate successful build*) |