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