equal
deleted
inserted
replaced
10 |
10 |
11 pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) |
11 pcpodef (open) ('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 syntax (xsymbols) |
15 type_notation (xsymbols) |
16 sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0) |
16 sfun (infixr "\<rightarrow>!" 0) |
17 |
17 |
18 text {* TODO: Define nice syntax for abstraction, application. *} |
18 text {* TODO: Define nice syntax for abstraction, application. *} |
19 |
19 |
20 definition |
20 definition |
21 sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)" |
21 sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)" |