src/HOL/HOLCF/Sfun.thy
changeset 49759 ecf1d5d87e5e
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
equal deleted inserted replaced
49758:718f10c8bbfc 49759:ecf1d5d87e5e
     6 
     6 
     7 theory Sfun
     7 theory Sfun
     8 imports Cfun
     8 imports Cfun
     9 begin
     9 begin
    10 
    10 
    11 pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
    11 pcpodef ('a, 'b) sfun (infixr "->!" 0)
    12   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    12   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    13 by simp_all
    13 by simp_all
    14 
    14 
    15 type_notation (xsymbols)
    15 type_notation (xsymbols)
    16   sfun  (infixr "\<rightarrow>!" 0)
    16   sfun  (infixr "\<rightarrow>!" 0)