| changeset 15577 | e16da3068ad6 |
| parent 15576 | efb95d0d01f7 |
| child 15589 | 69bea57212ef |
| 15576:efb95d0d01f7 | 15577:e16da3068ad6 |
|---|---|
7 |
7 |
8 *) |
8 *) |
9 |
9 |
10 header {* The type of continuous functions *} |
10 header {* The type of continuous functions *} |
11 |
11 |
12 theory Cfun = Cont: |
12 theory Cfun |
13 imports Cont |
|
14 begin |
|
13 |
15 |
14 defaultsort cpo |
16 defaultsort cpo |
15 |
17 |
16 typedef (CFun) ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}" |
18 typedef (CFun) ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}" |
17 by (rule exI, rule CfunI) |
19 by (rule exI, rule CfunI) |