changeset 2820 | 6303966dce96 |
child 4446 | 097004a470fb |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ex/ROOT.ML Thu Mar 20 11:09:01 1997 +0100 @@ -0,0 +1,10 @@ + +writeln"Root file for LCF examples"; +LCF_build_completed; (*Cause examples to fail if LCF did*) + +proof_timing := true; + +use"ex.ML"; + +cd ".."; +maketest"END: file for LCF examples";