--- a/src/HOLCF/Sprod.thy Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Sprod.thy Mon May 19 23:49:20 2008 +0200
@@ -230,14 +230,14 @@
subsection {* Strict product is a bifinite domain *}
-instance "**" :: (bifinite, bifinite) approx ..
+instantiation "**" :: (bifinite, bifinite) bifinite
+begin
-defs (overloaded)
+definition
approx_sprod_def:
- "approx \<equiv> \<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:)"
+ "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
-instance "**" :: (bifinite, bifinite) bifinite
-proof
+instance proof
fix i :: nat and x :: "'a \<otimes> 'b"
show "chain (\<lambda>i. approx i\<cdot>x)"
unfolding approx_sprod_def by simp
@@ -259,6 +259,8 @@
by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
qed
+end
+
lemma approx_spair [simp]:
"approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
unfolding approx_sprod_def