src/LCF/ex/ROOT.ML
author paulson
Sat, 10 Jan 1998 17:59:32 +0100
changeset 4552 bb8ff763c93d
parent 4446 097004a470fb
child 4905 be73ddff6c5a
permissions -rw-r--r--
Simplified proofs by omitting PA = {|XA, ...|} from RA2
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";