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/Derivative.thy
changeset 82486 451f428c5814
parent 80914 d97fdabd9e2b
child 82529 ff4b062aae57
child 82538 4b132ea7d575 
--- a/src/HOL/Analysis/Derivative.thy	Thu Apr 10 17:07:18 2025 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Apr 11 21:56:56 2025 +0100
@@ -2810,7 +2810,7 @@
         by simp
     qed
     have "\<exists>!x \<in> ?D. ?u x = x"
-    proof (rule banach_fix)
+    proof (rule Banach_fix)
       show "cball 0 \<delta> \<noteq> {}"
         using \<open>0 < \<delta>\<close> by auto
       show "(\<lambda>x. x + (y - f x)) ` cball 0 \<delta> \<subseteq> cball 0 \<delta>"
isabelle