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/Path_Connected.thy
changeset 71191 6695aeae8ec9
parent 71189 954ee5acaae0
parent 71184 d62fdaafdafc
child 71200 3548d54ce3ee 
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -4055,7 +4055,6 @@
   shows "\<exists>g. homeomorphism S T f g"
   using assms injective_into_1d_eq_homeomorphism by blast
 
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Rectangular paths\<close>
 
 definition\<^marker>\<open>tag unimportant\<close> rectpath where
isabelle