src/LCF/ex/ROOT.ML
author wenzelm
Fri, 19 Dec 1997 10:18:03 +0100
changeset 4446 097004a470fb
parent 2820 6303966dce96
child 4905 be73ddff6c5a
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     1
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     2
writeln"Root file for LCF examples";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     3
LCF_build_completed;    (*Cause examples to fail if LCF did*)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     4
4446
wenzelm
parents: 2820
diff changeset
     5
set proof_timing;
2820
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
wenzelm
parents:
diff changeset
     6
4446
wenzelm
parents: 2820
diff changeset
     7
use "ex.ML";