changeset 1696 | e84bff5c519b |
parent 1465 | 5d7a7e439cec |
child 4449 | df30e75f670f |
1695:0f9b9eda2a2c | 1696:e84bff5c519b |
---|---|
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 time_use_thy "Properties"; |
11 time_use_thy "Expr"; |
12 time_use_thy "Equiv"; |
12 time_use_thy "Transition"; |
13 time_use_thy "VC"; |
13 time_use_thy "VC"; |