author wenzelm
Sun, 18 Sep 2005 14:25:48 +0200
changeset 17480 fd19f77dcf60
parent 6349 f7750d816c21
child 25750 4e796867ccb5
permissions -rw-r--r--
converted to Isar theory format;

(*  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.

val banner = "First-Order Logic with Natural Deduction with Proof Terms";
writeln banner;

use_thy "FOLP";