src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 62343 24106dc44def
parent 61943 7fba644ed827
child 62390 842917225d56
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -711,7 +711,7 @@
     1.4  
     1.5  lemma card_of_UNION_Sigma:
     1.6  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
     1.7 -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
     1.8 +using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast
     1.9  
    1.10  lemma card_of_bool:
    1.11  assumes "a1 \<noteq> a2"