src/HOL/HOLCF/Cfun.thy
changeset 45695 b108b3d7c49e
parent 45606 b1e1508643b1
child 49759 ecf1d5d87e5e
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Wed Nov 30 16:27:10 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Wed Nov 30 17:30:01 2011 +0100
     1.3 @@ -13,8 +13,10 @@
     1.4  
     1.5  subsection {* Definition of continuous function type *}
     1.6  
     1.7 -cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
     1.8 -by (auto intro: cont_const adm_cont)
     1.9 +definition "cfun = {f::'a => 'b. cont f}"
    1.10 +
    1.11 +cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
    1.12 +  unfolding cfun_def by (auto intro: cont_const adm_cont)
    1.13  
    1.14  type_notation (xsymbols)
    1.15    cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)