| changeset 40502 | 8e92772bc0e8 |
| child 40592 | f432973ce0f6 |
| 40501:2ed71459136e | 40502:8e92772bc0e8 |
|---|---|
1 (* Title: HOLCF/Plain_HOLCF.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Plain HOLCF *} |
|
6 |
|
7 theory Plain_HOLCF |
|
8 imports Cfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix |
|
9 begin |
|
10 |
|
11 text {* |
|
12 Basic HOLCF concepts and types; does not include definition packages. |
|
13 *} |
|
14 |
|
15 end |