| changeset 35794 | 8cd7134275cc |
| parent 35641 | a17bc4cec23a |
| child 35914 | 91a7311177c4 |
| 35793:950d098c4a12 | 35794:8cd7134275cc |
|---|---|
1 (* Title: HOLCF/Cfun.thy |
1 (* Title: HOLCF/Cfun.thy |
2 Author: Franz Regensburger |
2 Author: Franz Regensburger |
3 |
3 Author: Brian Huffman |
4 Definition of the type -> of continuous functions. |
|
5 *) |
4 *) |
6 |
5 |
7 header {* The type of continuous functions *} |
6 header {* The type of continuous functions *} |
8 |
7 |
9 theory Cfun |
8 theory Cfun |