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/Brouwer_Fixpoint.thy
changeset 71745 ad84f8a712b4
parent 71449 3cf130a896a3
child 72302 d7d90ed4c74e 
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 10 22:51:18 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Apr 12 10:51:51 2020 +0100
@@ -149,7 +149,7 @@
     apply (rule_tac x=r in exI, simp)
      apply (rule homotopic_with_trans, assumption)
      apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
-        apply (rule_tac Y=S in homotopic_compose_continuous_left)
+        apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
          apply (auto simp: homotopic_with_sym)
     done
 qed
isabelle