src/FOLP/ROOT.ML
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 33615 261abc2e3155
permissions -rw-r--r--
clarified example settings for Proof General;

(*  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"];