--- a/src/HOLCF/Cprod.thy Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Cprod.thy Mon May 19 23:49:20 2008 +0200
@@ -342,14 +342,14 @@
subsection {* Product type is a bifinite domain *}
-instance "*" :: (profinite, profinite) approx ..
+instantiation "*" :: (profinite, profinite) profinite
+begin
-defs (overloaded)
+definition
approx_cprod_def:
- "approx \<equiv> \<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>"
+ "approx = (\<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>)"
-instance "*" :: (profinite, profinite) profinite
-proof
+instance proof
fix i :: nat and x :: "'a \<times> 'b"
show "chain (\<lambda>i. approx i\<cdot>x)"
unfolding approx_cprod_def by simp
@@ -367,6 +367,8 @@
intro finite_cartesian_product finite_fixes_approx)
qed
+end
+
instance "*" :: (bifinite, bifinite) bifinite ..
lemma approx_cpair [simp]: