src/HOLCF/Cfun.thy
changeset 35427 ad039d29e01c
parent 35168 07b3112e464b
child 35547 991a6af75978
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -23,8 +23,8 @@
     1.4  cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
     1.5  by (simp_all add: Ex_cont adm_cont)
     1.6  
     1.7 -syntax (xsymbols)
     1.8 -  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
     1.9 +type_notation (xsymbols)
    1.10 +  "->"  ("(_ \<rightarrow>/ _)" [1, 0] 0)
    1.11  
    1.12  notation
    1.13    Rep_CFun  ("(_$/_)" [999,1000] 999)