author | wenzelm |
Sat, 28 Jun 2008 22:52:03 +0200 | |
changeset 27388 | 226835ea8d2b |
parent 25750 | 4e796867ccb5 |
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";