| changeset 35427 | ad039d29e01c |
| parent 35167 | eba22d68a0a7 |
| child 35547 | 991a6af75978 |
--- a/src/HOLCF/ex/Strict_Fun.thy Tue Mar 02 23:56:13 2010 +0100 +++ b/src/HOLCF/ex/Strict_Fun.thy Tue Mar 02 23:59:54 2010 +0100 @@ -12,8 +12,8 @@ = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}" by simp_all -syntax (xsymbols) - sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0) +type_notation (xsymbols) + sfun (infixr "\<rightarrow>!" 0) text {* TODO: Define nice syntax for abstraction, application. *}