--- a/src/HOLCF/Cprod.thy Wed Mar 26 21:05:58 2008 +0100
+++ b/src/HOLCF/Cprod.thy Wed Mar 26 22:38:17 2008 +0100
@@ -342,13 +342,13 @@
subsection {* Product type is a bifinite domain *}
-instance "*" :: (bifinite_cpo, bifinite_cpo) approx ..
+instance "*" :: (profinite, profinite) approx ..
defs (overloaded)
approx_cprod_def:
"approx \<equiv> \<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>"
-instance "*" :: (bifinite_cpo, bifinite_cpo) bifinite_cpo
+instance "*" :: (profinite, profinite) profinite
proof
fix i :: nat and x :: "'a \<times> 'b"
show "chain (\<lambda>i. approx i\<cdot>x)"