changeset 49759 | ecf1d5d87e5e |
parent 42151 | 4da4fc77664b |
child 58880 | 0baae4311a9f |
--- a/src/HOL/HOLCF/Sfun.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Sfun.thy Tue Oct 09 17:33:46 2012 +0200 @@ -8,7 +8,7 @@ imports Cfun begin -pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) +pcpodef ('a, 'b) sfun (infixr "->!" 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}" by simp_all