src/HOL/Library/Old_Datatype.thy
changeset 61943 7fba644ed827
parent 61585 a9599d3d7610
child 61952 546958347e05
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -495,7 +495,7 @@
     1.4  
     1.5  (*** Bounding theorems ***)
     1.6  
     1.7 -lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
     1.8 +lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)"
     1.9  by blast
    1.10  
    1.11  lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
    1.12 @@ -505,7 +505,7 @@
    1.13      "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
    1.14  by auto
    1.15  
    1.16 -lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
    1.17 +lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)"
    1.18  by blast
    1.19  
    1.20  lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]