src/FOLP/ROOT.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 25750 4e796867ccb5
child 33615 261abc2e3155
permissions -rw-r--r--
use long names for old-style fold combinators;
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
wenzelm@25750
    11
use_thy "FOLP";
clasohm@0
    12