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/Lattices_Big.thy
changeset 82664 e9f3b94eb6a0
parent 80934 8e72f55295fd
child 82688 b391142bd2d2 
--- a/src/HOL/Lattices_Big.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/Lattices_Big.thy	Wed May 28 17:49:22 2025 +0200
@@ -783,7 +783,7 @@
     then obtain a where "f a = Max (f ` A)" and "a \<in> A"
       by (metis Max_in[of "f ` A"] imageE)
     then have "P (A - {a})"
-      using psubset member_remove by blast 
+      using psubset(2) [of \<open>A - {a}\<close>] by auto
     moreover 
     have "\<And>y. y \<in> A \<Longrightarrow> f y \<le> f a"
       using \<open>f a = Max (f ` A)\<close> \<open>finite (f ` A)\<close> by simp
isabelle