src/FOLP/ROOT.ML
author wenzelm
Sat, 28 Jun 2008 22:52:03 +0200
changeset 27388 226835ea8d2b
parent 25750 4e796867ccb5
child 33615 261abc2e3155
permissions -rw-r--r--
added ML/ml_thms.ML;

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

use_thy "FOLP";