equal
deleted
inserted
replaced
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 *} |
12 options [document = false] |
12 options [document = false] |
13 theories FOLP |
13 theories |
|
14 IFOLP (global) |
|
15 FOLP (global) |
14 |
16 |
15 session "FOLP-ex" in ex = FOLP + |
17 session "FOLP-ex" in ex = FOLP + |
16 description {* |
18 description {* |
17 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
19 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
18 Copyright 1992 University of Cambridge |
20 Copyright 1992 University of Cambridge |