equal
deleted
inserted
replaced
1 session FOLP! in "." = Pure + |
1 session FOLP = Pure + |
2 description {* |
2 description {* |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Modifed version of FOL that contains proof terms. |
6 Modifed version of FOL that contains proof terms. |
8 Presence of unknown proof term means that matching does not behave as expected. |
8 Presence of unknown proof term means that matching does not behave as expected. |
9 *} |
9 *} |
10 options [document = false] |
10 options [document = false] |
11 theories FOLP |
11 theories FOLP |
12 |
12 |
13 session ex = FOLP + |
13 session "FOLP-ex" in ex = FOLP + |
14 description {* |
14 description {* |
15 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
15 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
16 Copyright 1992 University of Cambridge |
16 Copyright 1992 University of Cambridge |
17 |
17 |
18 Examples for First-Order Logic. |
18 Examples for First-Order Logic. |