author | immler@in.tum.de |
Thu, 26 Feb 2009 10:13:43 +0100 | |
changeset 30151 | 629f3a92863e |
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 |