diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 26 22:11:55 2018 +0100
@@ -47,26 +47,6 @@
 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
   by auto
 
-lemma continuous_mult_left:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
-by (rule continuous_mult [OF continuous_const])
-
-lemma continuous_mult_right:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)"
-by (rule continuous_mult [OF _ continuous_const])
-
-lemma continuous_on_mult_left:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)"
-by (rule continuous_on_mult [OF continuous_on_const])
-
-lemma continuous_on_mult_right:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
-by (rule continuous_on_mult [OF _ continuous_on_const])
-
 lemma uniformly_continuous_on_cmul_right [continuous_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"