src/HOL/HOLCF/Cfun.thy
changeset 49759 ecf1d5d87e5e
parent 45695 b108b3d7c49e
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 16:58:36 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 17:33:46 2012 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  definition "cfun = {f::'a => 'b. cont f}"
     1.6  
     1.7 -cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
     1.8 +cpodef ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
     1.9    unfolding cfun_def by (auto intro: cont_const adm_cont)
    1.10  
    1.11  type_notation (xsymbols)