tuning
authorblanchet
Fri Jan 31 13:29:20 2014 +0100 (2014-01-31)
changeset 55206f7358e55018f
parent 55205 8450622db0c5
child 55207 42ad887a1c7c
tuning
src/HOL/BNF_Cardinal_Order_Relation.thy
     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