src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 56075 c6d4425f1fdc
parent 56011 39d5043ce8a3
child 56077 d397030fb27e
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:07 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:08 2014 +0100
     1.3 @@ -711,7 +711,7 @@
     1.4  
     1.5  corollary card_of_Sigma_Times:
     1.6  "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
     1.7 -using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .
     1.8 +by (fact card_of_Sigma_mono1)
     1.9  
    1.10  lemma card_of_UNION_Sigma:
    1.11  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"