| changeset 48475 | 02dd825f5a4e |
| child 48483 | 9bfb6978eb80 |
| 48474:5b9d79c6323b | 48475:02dd825f5a4e |
|---|---|
1 session LCF! in "." = Pure + |
|
2 description {* |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1992 University of Cambridge |
|
5 *} |
|
6 theories LCF |
|
7 |
|
8 session ex = LCF + |
|
9 description {* |
|
10 Author: Tobias Nipkow |
|
11 Copyright 1991 University of Cambridge |
|
12 |
|
13 Some examples from Lawrence Paulson's book Logic and Computation. |
|
14 *} |
|
15 theories Ex1 Ex2 Ex3 Ex4 |
|
16 |