src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
changeset 67399 eab6ce8368fa
parent 66703 61bf958fa1c1
child 67613 ce654b0e6d69
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -1041,10 +1041,10 @@
       and eq1: "\<And>c x. \<lbrakk>(a + c *\<^sub>R x) \<in> S; 0 \<le> c; a + x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
     shows "negligible S"
 proof -
-  have "negligible (op + (-a) ` S)"
+  have "negligible ((+) (-a) ` S)"
   proof (subst negligible_on_intervals, intro allI)
     fix u v
-    show "negligible (op + (- a) ` S \<inter> cbox u v)"
+    show "negligible ((+) (- a) ` S \<inter> cbox u v)"
       unfolding negligible_iff_null_sets
       apply (rule starlike_negligible_compact)
        apply (simp add: assms closed_translation closed_Int_compact, clarify)
@@ -1831,7 +1831,7 @@
           qed
           also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> snd ` p. norm (integral (i\<inter>l) f))"
             by (simp add: sum.cartesian_product)
-          also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod op \<inter> x) f))"
+          also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod (\<inter>) x) f))"
             by (force simp: split_def intro!: sum.cong)
           also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
           proof -