src/FOLP/ROOT.ML
author haftmann
Tue Sep 20 08:21:49 2005 +0200 (2005-09-20)
changeset 17496 26535df536ae
parent 17480 fd19f77dcf60
child 25750 4e796867ccb5
permissions -rw-r--r--
slight adaptions to library changes
wenzelm@17480
     1
(*  Title:      FOLP/ROOT.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Modifed version of Lawrence Paulson's FOL that contains proof terms.
clasohm@0
     7
clasohm@0
     8
Presence of unknown proof term means that matching does not behave as expected.
clasohm@0
     9
*)
clasohm@0
    10
clasohm@0
    11
val banner = "First-Order Logic with Natural Deduction with Proof Terms";
clasohm@0
    12
writeln banner;
clasohm@0
    13
clasohm@98
    14
use_thy "FOLP";