changeset 27310 | d0229bc6c461 |
parent 26962 | c8b20f615d6c |
child 27413 | 3154f3765cc7 |
--- a/src/HOLCF/Cprod.thy Fri Jun 20 22:51:50 2008 +0200 +++ b/src/HOLCF/Cprod.thy Fri Jun 20 23:01:09 2008 +0200 @@ -351,7 +351,7 @@ instance proof fix i :: nat and x :: "'a \<times> 'b" - show "chain (\<lambda>i. approx i\<cdot>x)" + show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)" unfolding approx_cprod_def by simp show "(\<Squnion>i. approx i\<cdot>x) = x" unfolding approx_cprod_def