| changeset 1142 | eb0e2ff8f032 |
| parent 0 | a5a9c433f639 |
| child 1477 | 4c51ab632cda |
| 1141:a94c0ab9a3ed | 1142:eb0e2ff8f032 |
|---|---|
1 (* Title: FOLP/FOLP.thy |
|
2 ID: $Id$ |
|
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Classical First-Order Logic with Proofs |
|
7 *) |
|
8 |
|
1 FOLP = IFOLP + |
9 FOLP = IFOLP + |
2 consts |
10 consts |
3 cla :: "[p=>p]=>p" |
11 cla :: "[p=>p]=>p" |
4 rules |
12 rules |
5 classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P" |
13 classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P" |