src/FOLP/ROOT.ML
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 33615 261abc2e3155
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

(*  Title:      FOLP/ROOT.ML
    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_thys ["FOLP"];