| author | nipkow | 
| Wed, 30 Jul 2008 16:07:00 +0200 | |
| changeset 27712 | 007a339b9e7d | 
| parent 25750 | 4e796867ccb5 | 
| child 33615 | 261abc2e3155 | 
| permissions | -rw-r--r-- | 
| 17480 | 1  | 
(* Title: FOLP/ROOT.ML  | 
| 0 | 2  | 
ID: $Id$  | 
| 1459 | 3  | 
Author: martin Coen, Cambridge University Computer Laboratory  | 
| 0 | 4  | 
Copyright 1993 University of Cambridge  | 
5  | 
||
6  | 
Modifed version of Lawrence Paulson's FOL that contains proof terms.  | 
|
7  | 
||
8  | 
Presence of unknown proof term means that matching does not behave as expected.  | 
|
9  | 
*)  | 
|
10  | 
||
| 25750 | 11  | 
use_thy "FOLP";  | 
| 0 | 12  |