src/HOL/Analysis/Bochner_Integration.thy

     using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
 
   have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))"
     using s t by (subst simple_bochner_integral_diff) auto
   also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))"
-    using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t
+    using simple_bochner_integrable_compose2[of "(-)" M "s" "t"] s t
     by (auto intro!: simple_bochner_integral_norm_bound)
   also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
     using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
     by (auto intro!: simple_bochner_integral_eq_nn_integral)
   also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)"

   then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x"
     by simp
 
   have sf[measurable]: "\<And>i. simple_function M (s' i)"
     unfolding s'_def using s(1)
-    by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto
+    by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto
 
   { fix i
     have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
         (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})"
       by (auto simp add: s'_def split: split_indicator)

   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
     and nn: "AE x in M. 0 \<le> g x"
   shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
   unfolding integrable_iff_bounded using nn
   apply (simp add: nn_integral_density less_top[symmetric])
-  apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
+  apply (intro arg_cong2[where f="(=)"] refl nn_integral_cong_AE)
   apply (auto simp: ennreal_mult)
   done
 
 lemma integral_density:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"