changeset 1351 | 4a960c012383 |
parent 1340 | 71b0a5d83347 |
child 1447 | bc2c0acbbf29 |
1350:5bf4a54ba25f | 1351:4a960c012383 |
---|---|
6 |
6 |
7 HOL_build_completed; (*Make examples fail if HOL did*) |
7 HOL_build_completed; (*Make examples fail if HOL did*) |
8 |
8 |
9 writeln"Root file for HOL/IMP"; |
9 writeln"Root file for HOL/IMP"; |
10 proof_timing := true; |
10 proof_timing := true; |
11 loadpath := [".","IMP"]; |
|
12 time_use_thy "Properties"; |
11 time_use_thy "Properties"; |
13 time_use_thy "Equiv"; |
12 time_use_thy "Equiv"; |
14 time_use_thy "Hoare"; |
13 time_use_thy "Hoare"; |
15 |
|
16 make_chart (); (*make HTML chart*) |