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