--- a/src/HOL/Analysis/Starlike.thy Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Starlike.thy Fri Feb 02 11:25:11 2024 +0000
@@ -4354,7 +4354,7 @@
have cont_f: "continuous_on (affine hull S) f"
proof (clarsimp simp: dist_norm continuous_on_iff diff)
show "\<And>x e. 0 < e \<Longrightarrow> \<exists>d>0. \<forall>y \<in> affine hull S. \<bar>f y - f x\<bar> * norm z < d \<longrightarrow> \<bar>f y - f x\<bar> < e"
- by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_iff1 zero_less_norm_iff)
+ by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_cancel_right_pos zero_less_norm_iff)
qed
then have conn_fS: "connected (f ` S)"
by (meson S connected_continuous_image continuous_on_subset hull_subset)
@@ -4424,7 +4424,7 @@
have cont_f: "continuous_on (affine hull S) f"
proof (clarsimp simp: dist_norm continuous_on_iff diff)
show "\<And>x e. 0 < e \<Longrightarrow> \<exists>d>0. \<forall>y \<in> affine hull S. \<bar>f y - f x\<bar> * norm z < d \<longrightarrow> \<bar>f y - f x\<bar> < e"
- by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_iff1 zero_less_norm_iff)
+ by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_cancel_right_pos zero_less_norm_iff)
qed
then have "connected (f ` S)"
by (meson \<open>connected S\<close> connected_continuous_image continuous_on_subset hull_subset)