src/HOL/Real_Vector_Spaces.thy

   obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
   by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
 
 corollary real_linearD:
   fixes f :: "real \<Rightarrow> real"
-  assumes "linear f" obtains c where "f = op* c"
+  assumes "linear f" obtains c where "f = ( * ) c"
   by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
 
 lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
   apply (simp add: linear_def Real_Vector_Spaces.additive_def linear_axioms_def)
   by (metis distrib_left mult_scaleR_right scaleR_conv_of_real)

   apply blast
   done
 
 lemma comp1:
   assumes "bounded_linear g"
-  shows "bounded_bilinear (\<lambda>x. op ** (g x))"
+  shows "bounded_bilinear (\<lambda>x. ( ** ) (g x))"
 proof unfold_locales
   interpret g: bounded_linear g by fact
   show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
     "\<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'"
     "\<And>r a b. g (r *\<^sub>R a) ** b = r *\<^sub>R (g a ** b)"

       finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
     qed
   qed
 qed
 
-lemma bounded_bilinear_mult: "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
+lemma bounded_bilinear_mult: "bounded_bilinear (( * ) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
   apply (rule bounded_bilinear.intro)
       apply (rule distrib_right)
      apply (rule distrib_left)
     apply (rule mult_scaleR_left)
    apply (rule mult_scaleR_right)