equal
deleted
inserted
replaced
1 session LCF! in "." = Pure + |
1 session LCF! in "." = Pure + |
2 description {* |
2 description {* |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 *} |
5 *} |
|
6 options [document = false] |
6 theories LCF |
7 theories LCF |
7 |
8 |
8 session ex = LCF + |
9 session ex = LCF + |
9 description {* |
10 description {* |
10 Author: Tobias Nipkow |
11 Author: Tobias Nipkow |
11 Copyright 1991 University of Cambridge |
12 Copyright 1991 University of Cambridge |
12 |
13 |
13 Some examples from Lawrence Paulson's book Logic and Computation. |
14 Some examples from Lawrence Paulson's book Logic and Computation. |
14 *} |
15 *} |
15 theories Ex1 Ex2 Ex3 Ex4 |
16 options [document = false] |
|
17 theories |
|
18 Ex1 |
|
19 Ex2 |
|
20 Ex3 |
|
21 Ex4 |
16 |
22 |