| changeset 4446 | 097004a470fb |
| parent 2820 | 6303966dce96 |
| child 4905 | be73ddff6c5a |
| 4445:de74b549f976 | 4446:097004a470fb |
|---|---|
1 |
1 |
2 writeln"Root file for LCF examples"; |
2 writeln"Root file for LCF examples"; |
3 LCF_build_completed; (*Cause examples to fail if LCF did*) |
3 LCF_build_completed; (*Cause examples to fail if LCF did*) |
4 |
4 |
5 proof_timing := true; |
5 set proof_timing; |
6 |
6 |
7 use"ex.ML"; |
7 use "ex.ML"; |
8 |
|
9 cd ".."; |
|
10 maketest"END: file for LCF examples"; |