changeset 25750 | 4e796867ccb5 |
parent 17247 | 6927a62c77dc |
child 33615 | 261abc2e3155 |
25749:10e7feb4e595 | 25750:4e796867ccb5 |
---|---|
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 val banner = "Logic for Computable Functions (in FOL)"; |
7 use_thy "LCF"; |
8 writeln banner; |
|
9 |
8 |
10 use_thy "LCF"; |