Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning
authorblanchet
Fri, 31 Jan 2014 13:29:20 +0100
changeset 55206 f7358e55018f
parent 55205 8450622db0c5
child 55207 42ad887a1c7c
tuning
src/HOL/BNF_Cardinal_Order_Relation.thy file | annotate | diff | comparison | revisions 
--- 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