equal
deleted
inserted
replaced
11 |
11 |
12 default_sort cpo |
12 default_sort cpo |
13 |
13 |
14 subsection {* Definition of continuous function type *} |
14 subsection {* Definition of continuous function type *} |
15 |
15 |
16 cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}" |
16 definition "cfun = {f::'a => 'b. cont f}" |
17 by (auto intro: cont_const adm_cont) |
17 |
|
18 cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set" |
|
19 unfolding cfun_def by (auto intro: cont_const adm_cont) |
18 |
20 |
19 type_notation (xsymbols) |
21 type_notation (xsymbols) |
20 cfun ("(_ \<rightarrow>/ _)" [1, 0] 0) |
22 cfun ("(_ \<rightarrow>/ _)" [1, 0] 0) |
21 |
23 |
22 notation |
24 notation |