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/Library/Equipollence.thy
changeset 73932 fd21b4a93043
parent 71857 d73955442df5
child 75331 c3f1bf2824bc 
--- a/src/HOL/Library/Equipollence.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Equipollence.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -125,7 +125,7 @@
   show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
     using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
   show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
-  by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
+  by (metis (no_types, opaque_lifting) image_empty image_insert lepoll_iff that)
 qed
 
 lemma infinite_insert_lepoll:
isabelle