src/FOLP/ROOT.ML
author wenzelm
Sat, 10 Jan 2009 21:32:30 +0100
changeset 29435 a5f84ac14609
parent 25750 4e796867ccb5
child 33615 261abc2e3155
permissions -rw-r--r--
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

(*  Title:      FOLP/ROOT.ML
    ID:         $Id$
    Author:     martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Modifed version of Lawrence Paulson's FOL that contains proof terms.

Presence of unknown proof term means that matching does not behave as expected.
*)

use_thy "FOLP";