| changeset 1142 | eb0e2ff8f032 |
| parent 648 | e27c9ec2b48b |
| child 1149 | 5750eba8820d |
| 1141:a94c0ab9a3ed | 1142:eb0e2ff8f032 |
|---|---|
1 (* Title: FOLP/IFOLP.thy |
|
2 ID: $Id$ |
|
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Intuitionistic First-Order Logic with Proofs |
|
7 *) |
|
8 |
|
1 IFOLP = Pure + |
9 IFOLP = Pure + |
2 |
10 |
3 classes term < logic |
11 classes term < logic |
4 |
12 |
5 default term |
13 default term |