src/HOLCF/Sprod.thy
changeset 39986 38677db30cad
parent 39985 310f98585107
child 39987 8c2f449af35a
     1.1 --- a/src/HOLCF/Sprod.thy	Thu Oct 07 13:54:43 2010 -0700
     1.2 +++ b/src/HOLCF/Sprod.thy	Fri Oct 08 07:39:50 2010 -0700
     1.3 @@ -310,7 +310,7 @@
     1.4      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
     1.5  qed
     1.6  
     1.7 -subsection {* Strict product is an SFP domain *}
     1.8 +subsection {* Strict product is a bifinite domain *}
     1.9  
    1.10  definition
    1.11    sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    1.12 @@ -342,7 +342,7 @@
    1.13  apply (erule (1) finite_deflation_sprod_map)
    1.14  done
    1.15  
    1.16 -instantiation sprod :: (sfp, sfp) sfp
    1.17 +instantiation sprod :: (bifinite, bifinite) bifinite
    1.18  begin
    1.19  
    1.20  definition
    1.21 @@ -367,9 +367,8 @@
    1.22  
    1.23  end
    1.24  
    1.25 -text {* SFP of type constructor = type combinator *}
    1.26 -
    1.27 -lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.28 +lemma SFP_sprod:
    1.29 +  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.30  by (rule sfp_sprod_def)
    1.31  
    1.32  end