| author | wenzelm |
| Thu, 07 Jul 2011 23:55:15 +0200 | |
| changeset 44572 | 91c4d7397f0e |
| parent 33615 | 261abc2e3155 |
| permissions | -rw-r--r-- |
1 (* Title: FOLP/ROOT.ML
2 Author: Martin Coen, Cambridge University Computer Laboratory
3 Copyright 1993 University of Cambridge
5 Modifed version of Lawrence Paulson's FOL that contains proof terms.
7 Presence of unknown proof term means that matching does not behave as expected.
8 *)
10 use_thys ["FOLP"];