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


writeln"Root file for LCF examples";
LCF_build_completed;    (*Cause examples to fail if LCF did*)

set proof_timing;

use "ex.ML";