| changeset 17817 | 405fb812e738 |
| parent 17816 | 9942c5ed866a |
| child 17832 | e18fc1a9a0e0 |
--- a/src/HOLCF/Cfun.thy Mon Oct 10 05:30:02 2005 +0200 +++ b/src/HOLCF/Cfun.thy Mon Oct 10 05:46:17 2005 +0200 @@ -22,7 +22,7 @@ lemma adm_cont: "adm cont" by (rule admI, rule cont_lub_fun) -cpodef (CFun) ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}" +cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}" by (simp add: Ex_cont adm_cont) syntax (xsymbols)