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