| changeset 29063 | 7619f0561cd7 |
| parent 29049 | 4e5b9e508e1e |
| child 29138 | 661a8db7e647 |
--- a/src/HOLCF/Cfun.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Cfun.thy Thu Dec 11 16:50:18 2008 +0100 @@ -23,7 +23,7 @@ by (rule admI, rule cont_lub_fun) cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}" -by (simp add: Ex_cont adm_cont) +by (simp_all add: Ex_cont adm_cont) syntax (xsymbols) "->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)