| changeset 40774 | 0437dbc127b3 |
| parent 40773 | 6c12f5e24e34 |
| child 40775 | ed7a4eadb2f6 |
| 40773:6c12f5e24e34 | 40774:0437dbc127b3 |
|---|---|
1 (* Title: HOLCF/Plain_HOLCF.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Plain HOLCF *} |
|
6 |
|
7 theory Plain_HOLCF |
|
8 imports Cfun Sfun 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 |