--- a/src/HOLCF/Sprod.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Sprod.thy Fri Oct 08 07:39:50 2010 -0700
@@ -310,7 +310,7 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict product is an SFP domain *}
+subsection {* Strict product is a bifinite domain *}
definition
sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
@@ -342,7 +342,7 @@
apply (erule (1) finite_deflation_sprod_map)
done
-instantiation sprod :: (sfp, sfp) sfp
+instantiation sprod :: (bifinite, bifinite) bifinite
begin
definition
@@ -367,9 +367,8 @@
end
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_sprod:
+ "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_sprod_def)
end