src/HOL/Limits.thy

   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
 by (rule continuous_on_mult [OF _ continuous_on_const])
 
 lemma continuous_on_mult_const [simp]:
   fixes c::"'a::real_normed_algebra"
-  shows "continuous_on s (( *) c)"
+  shows "continuous_on s ((*) c)"
   by (intro continuous_on_mult_left continuous_on_id)
 
 lemma tendsto_divide_zero:
   fixes c :: "'a::real_normed_field"
   shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F"