author | wenzelm |
Mon, 31 Dec 2007 19:36:29 +0100 | |
changeset 25750 | 4e796867ccb5 |
parent 17480 | fd19f77dcf60 |
child 33615 | 261abc2e3155 |
permissions | -rw-r--r-- |
(* 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";