src/HOL/Analysis/Gamma_Function.thy

       finally show "?g n = ?h n" by (simp only: mult_ac)
     qed
 
     moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
     hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
-      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
+      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "( * )2" "2*z"]
       by (intro tendsto_intros Gamma_series'_LIMSEQ)
          (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
     ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
       by (rule Lim_transform_eventually)
   } note lim = this

   also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) * 
                               (u - t) powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
   proof (rule nn_integral_cong, goal_cases)
     case (1 t)
     have "(\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{0..}) (t,u) * t powr (a - 1) * 
-                              u powr (b - 1) / exp (t + u)) \<partial>distr lborel borel (op + (-t))) =
+                              u powr (b - 1) / exp (t + u)) \<partial>distr lborel borel ((+) (-t))) =
                (\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) * 
                               (u - t) powr (b - 1) / exp u) \<partial>lborel)"
       by (subst nn_integral_distr) (auto intro!: nn_integral_cong simp: indicator_def)
     thus ?case by (subst (asm) lborel_distr_plus)
   qed

     show ?case
     proof (cases "u > 0")
       case True
       have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) = 
               (\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1)) 
-                \<partial>distr lborel borel (op * (1 / u)))" (is "_ = nn_integral _ ?f")
+                \<partial>distr lborel borel (( * ) (1 / u)))" (is "_ = nn_integral _ ?f")
         using True
         by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
-      also have "distr lborel borel (op * (1 / u)) = density lborel (\<lambda>_. u)"
+      also have "distr lborel borel (( * ) (1 / u)) = density lborel (\<lambda>_. u)"
         using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
       also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
                                               (u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
         by (subst nn_integral_density) (auto simp: ennreal_mult' [symmetric] algebra_simps)
       also have "\<dots> = (\<integral>\<^sup>+x. ennreal (u powr (a + b - 1)) *