highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;
session LCF = Pure +
description {*
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
*}
options [document = false]
theories LCF
session "LCF-ex" in ex = LCF +
description {*
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Some examples from Lawrence Paulson's book Logic and Computation.
*}
options [document = false]
theories
Ex1
Ex2
Ex3
Ex4