| changeset 29138 | 661a8db7e647 |
| parent 27419 | ff2a2b8fcd09 |
| child 31076 | 99fe356cbbc2 |
| 29131:fd8bb7527f7b | 29138:661a8db7e647 |
|---|---|
1 (* Title: HOLCF/FunCpo.thy |
1 (* Title: HOLCF/FunCpo.thy |
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
2 Author: Franz Regensburger |
4 |
|
5 Definition of the partial ordering for the type of all functions => (fun) |
|
6 |
|
7 Class instance of => (fun) for class pcpo. |
|
8 *) |
3 *) |
9 |
4 |
10 header {* Class instances for the full function space *} |
5 header {* Class instances for the full function space *} |
11 |
6 |
12 theory Ffun |
7 theory Ffun |