changeset 41022 | 0437dbc127b3 |
parent 40840 | f432973ce0f6 |
41021:6c12f5e24e34 | 41022: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 |