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.
prefer existing proof in Abstract_Topological_Spaces
authornipkow
Wed, 13 Aug 2025 09:34:57 +0200
changeset 83004 304519f22c2c
parent 83002 7ac70210d12c (current diff)
parent 83003 1ee42e4832aa (diff)
child 83005 a2a860cd3215
prefer existing proof in Abstract_Topological_Spaces
src/HOL/Analysis/Abstract_Topological_Spaces.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Aug 13 08:54:01 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Aug 13 09:34:57 2025 +0200
@@ -954,8 +954,8 @@
   show ?thesis
   proof
     assume ?lhs
-    with r show ?rhs
-      by (metis Pi_I' imageI invertible_fixpoint_property[of T i S r])
+    with r Pi_I' imageI invertible_fixpoint_property[of T i S r] show ?rhs
+      by metis
   next
     assume ?rhs
     with r show ?lhs
isabelle