equal
deleted
inserted
replaced
|
1 session FOLP! in "." = Pure + |
|
2 description {* |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Modifed version of FOL that contains proof terms. |
|
7 |
|
8 Presence of unknown proof term means that matching does not behave as expected. |
|
9 *} |
|
10 theories FOLP |
|
11 |
|
12 session ex = FOLP + |
|
13 description {* |
|
14 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
15 Copyright 1992 University of Cambridge |
|
16 |
|
17 Examples for First-Order Logic. |
|
18 *} |
|
19 theories |
|
20 Intro |
|
21 Nat |
|
22 Foundation |
|
23 If |
|
24 Intuitionistic |
|
25 Classical |
|
26 Propositional_Int |
|
27 Quantifiers_Int |
|
28 Propositional_Cla |
|
29 Quantifiers_Cla |
|
30 |