Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 55206 f7358e55018f
parent 55101 57c875e488bd
child 55603 48596c45bf7f 
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jan 31 12:30:54 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jan 31 13:29:20 2014 +0100
@@ -746,7 +746,7 @@
      qed
     }
     ultimately show ?thesis unfolding bij_betw_def inj_on_def
-    by (metis image_subsetI order_eq_iff subsetI)
+    by (metis (no_types) image_subsetI order_eq_iff subsetI)
   qed
   thus ?thesis using card_of_ordIso by blast
 qed
isabelle