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/Analysis/Lindelof_Spaces.thy
changeset 78248 740b23f1138a
parent 76063 24c9f56aa035
child 78336 6bae28577994 
--- a/src/HOL/Analysis/Lindelof_Spaces.thy	Sun Jul 02 14:28:20 2023 +0200
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy	Mon Jul 03 11:45:59 2023 +0100
@@ -253,7 +253,7 @@
         show "x \<in> \<Union> (\<Union> (\<V> ` I))" if "x \<in> topspace X" for x
         proof -
           have "f x \<in> topspace Y"
-            by (meson f image_subset_iff proper_map_imp_subset_topspace that)
+            using f proper_map_imp_subset_topspace that by fastforce
           then show ?thesis
             using that I by auto
         qed
isabelle