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 78320 eb9a9690b8f5
parent 78248 740b23f1138a
child 78336 6bae28577994 
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Jul 10 18:48:22 2023 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jul 11 20:21:58 2023 +0100
@@ -4026,7 +4026,7 @@
         qed auto
       qed
       then show "continuous_map (top_of_set ?S) X g"
-        by (simp add: continuous_map_def gf)
+        by (simp add: "1" continuous_map)
     qed (auto simp: gf)
   qed
 qed
isabelle