changeset 1351 | 4a960c012383 |
parent 1300 | c7a8f374339b |
child 1925 | 1150f128c7fe |
1350:5bf4a54ba25f | 1351:4a960c012383 |
---|---|
7 *) |
7 *) |
8 |
8 |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
10 |
10 |
11 writeln"Root file for HOL/MiniML"; |
11 writeln"Root file for HOL/MiniML"; |
12 loadpath := [".","MiniML"]; |
|
13 Unify.trace_bound := 20; |
12 Unify.trace_bound := 20; |
14 |
13 |
15 time_use_thy "I"; |
14 time_use_thy "I"; |
16 |
|
17 make_chart (); (*make HTML chart*) |