changeset 4583 | 6d9be46ea566 |
parent 4446 | 097004a470fb |
child 6349 | f7750d816c21 |
4582:c5cfd00e4f28 | 4583:6d9be46ea566 |
---|---|
2 writeln"Root file for Cube examples"; |
2 writeln"Root file for Cube examples"; |
3 Cube_build_completed; (*Cause examples to fail if Cube did*) |
3 Cube_build_completed; (*Cause examples to fail if Cube did*) |
4 |
4 |
5 set proof_timing; |
5 set proof_timing; |
6 |
6 |
7 use "ex.ML"; |
7 use_thy "ex"; |