| changeset 65378 | 4bb51e6334ed |
| parent 45049 | 13efaee97111 |
| 65377:6e47a27e3d43 | 65378:4bb51e6334ed |
|---|---|
1 (* Title: HOL/HOLCF/HOLCF.thy |
1 (* Title: HOL/HOLCF/HOLCF.thy |
2 Author: Franz Regensburger |
2 Author: Franz Regensburger |
3 Author: Brian Huffman |
|
3 |
4 |
4 HOLCF -- a semantic extension of HOL by the LCF logic. |
5 HOLCF -- a semantic extension of HOL by the LCF logic. |
5 *) |
6 *) |
6 |
7 |
7 theory HOLCF |
8 theory HOLCF |