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 79566 f783490c6c99
parent 78700 4de5b127c124 
--- a/src/HOL/Analysis/Derivative.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -1116,7 +1116,7 @@
         have "norm (g z - g y) < d0"
           by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) \<open>0 < d0\<close> d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff)
         then show ?thesis
-          by (metis C(1) \<open>y \<in> T\<close> d0 fg mult_le_cancel_iff1)
+          by (metis C(1) \<open>y \<in> T\<close> d0 fg mult_le_cancel_right_pos)
       qed
       also have "\<dots> \<le> e * norm (g z - g y)"
         using C by (auto simp add: field_simps)
isabelle