| changeset 16070 | 4a83dd540b88 |
| parent 15599 | 10cedbd5289e |
| child 16215 | 7ff978ca1920 |
| 16069:3f2a9f400168 | 16070:4a83dd540b88 |
|---|---|
1 (* Title: HOLCF/Up.thy |
1 (* Title: HOLCF/Up.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger and Brian Huffman |
4 Additions by Brian Huffman |
|
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6 |
4 |
7 Lifting. |
5 Lifting. |
8 *) |
6 *) |
9 |
7 |
10 header {* The type of lifted values *} |
8 header {* The type of lifted values *} |