src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 55603 48596c45bf7f
parent 55206 f7358e55018f
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 20 11:40:03 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 20 13:53:26 2014 +0100
     1.3 @@ -414,7 +414,7 @@
     1.4    let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
     1.5    have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
     1.6    using * unfolding inj_on_def by auto
     1.7 -  thus ?thesis using card_of_ordLeq by fast
     1.8 +  thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
     1.9  qed
    1.10  
    1.11  corollary Card_order_singl_ordLeq: