src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 55206 f7358e55018f
parent 55101 57c875e488bd
child 55603 48596c45bf7f
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jan 31 12:30:54 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jan 31 13:29:20 2014 +0100
     1.3 @@ -746,7 +746,7 @@
     1.4       qed
     1.5      }
     1.6      ultimately show ?thesis unfolding bij_betw_def inj_on_def
     1.7 -    by (metis image_subsetI order_eq_iff subsetI)
     1.8 +    by (metis (no_types) image_subsetI order_eq_iff subsetI)
     1.9    qed
    1.10    thus ?thesis using card_of_ordIso by blast
    1.11  qed