| changeset 16070 | 4a83dd540b88 |
| parent 16055 | 58186c507750 |
| child 16085 | c004b9bc970e |
| 16069:3f2a9f400168 | 16070:4a83dd540b88 |
|---|---|
1 (* Title: HOLCF/Cfun.thy |
1 (* Title: HOLCF/Cfun.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
4 |
6 Definition of the type -> of continuous functions. |
5 Definition of the type -> of continuous functions. |
7 |
|
8 *) |
6 *) |
9 |
7 |
10 header {* The type of continuous functions *} |
8 header {* The type of continuous functions *} |
11 |
9 |
12 theory Cfun |
10 theory Cfun |