# HG changeset patch
# User nipkow
# Date 1524765092 -7200
# Node ID 6aba668aea78d69d27297b356509450dbec97bc0
# Parent  d45b78cb86cffec4f3b4e87db3c3f0c520d0401d
new simp modifier: reorient

diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -474,8 +474,8 @@
     by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ennreal (f x)" and v=enn2real])
        (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
              intro!: sum.cong ennreal_cong_mult
-             simp: sum_ennreal[symmetric] ac_simps ennreal_mult
-             simp del: sum_ennreal)
+             simp: ac_simps ennreal_mult
+             reorient: sum_ennreal)
   also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
     using f
     by (intro nn_integral_eq_simple_integral[symmetric])
@@ -503,7 +503,7 @@
     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)"
-    by (auto intro!: nn_integral_mono simp: ennreal_plus[symmetric] simp del: ennreal_plus)
+    by (auto intro!: nn_integral_mono reorient: ennreal_plus)
        (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
               norm_minus_commute norm_triangle_ineq4 order_refl)
   also have "\<dots> = ?S + ?T"
@@ -593,7 +593,7 @@
     proof (intro always_eventually allI)
       fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) \<partial>M)"
         by (auto intro!: nn_integral_mono norm_diff_triangle_ineq
-                 simp del: ennreal_plus simp add: ennreal_plus[symmetric])
+                 reorient: ennreal_plus)
       also have "\<dots> = ?g i"
         by (intro nn_integral_add) auto
       finally show "?f i \<le> ?g i" .
@@ -746,7 +746,7 @@
   finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
 
   have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) + ennreal (norm (s i x)) \<partial>M)"
-    by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
+    by (auto intro!: nn_integral_mono reorient: ennreal_plus)
        (metis add.commute norm_triangle_sub)
   also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
     by (rule nn_integral_add) auto
@@ -782,7 +782,7 @@
         by (intro simple_bochner_integral_eq_nn_integral)
            (auto intro: s simple_bochner_integrable_compose2)
       also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s n x)) + norm (f x) \<partial>M)"
-        by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
+        by (auto intro!: nn_integral_mono reorient: ennreal_plus)
            (metis add.commute norm_minus_commute norm_triangle_sub)
       also have "\<dots> = ?t n"
         by (rule nn_integral_add) auto
@@ -827,7 +827,7 @@
       using tendsto_add[OF \<open>?S \<longlonglongrightarrow> 0\<close> \<open>?T \<longlonglongrightarrow> 0\<close>] by simp
   qed
   then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> 0"
-    by (simp add: ennreal_0[symmetric] del: ennreal_0)
+    by (simp reorient: ennreal_0)
   ultimately have "norm (x - y) = 0"
     by (rule LIMSEQ_unique)
   then show "x = y" by simp
@@ -1173,7 +1173,7 @@
         by (intro simple_bochner_integral_bounded s f)
       also have "\<dots> < ennreal (e / 2) + e / 2"
         by (intro add_strict_mono M n m)
-      also have "\<dots> = e" using \<open>0<e\<close> by (simp del: ennreal_plus add: ennreal_plus[symmetric])
+      also have "\<dots> = e" using \<open>0<e\<close> by (simp reorient: ennreal_plus)
       finally show "dist (?s n) (?s m) < e"
         using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
     qed
@@ -1218,7 +1218,7 @@
       fix x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
       from tendsto_diff[OF tendsto_const[of "u' x"] this]
       show "(\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
-        by (simp add: tendsto_norm_zero_iff ennreal_0[symmetric] del: ennreal_0)
+        by (simp add: tendsto_norm_zero_iff reorient: ennreal_0)
     qed
   qed (insert bnd w_nonneg, auto)
   then show ?thesis by simp
@@ -2116,7 +2116,7 @@
       by auto
   qed
   then have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F"
-    by (simp add: ennreal_0[symmetric] del: ennreal_0)
+    by (simp reorient: ennreal_0)
   then have "((\<lambda>n. ((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F" using tendsto_norm_zero_iff by blast
   then show ?thesis using Lim_null by auto
 qed
@@ -2214,7 +2214,7 @@
     ultimately have "(\<lambda>n. ennreal (norm(u (r n) x))) \<longlonglongrightarrow> 0"
       using tendsto_Limsup[of sequentially "\<lambda>n. ennreal (norm(u (r n) x))"] by auto
     then have "(\<lambda>n. norm(u (r n) x)) \<longlonglongrightarrow> 0"
-      by (simp add: ennreal_0[symmetric] del: ennreal_0)
+      by (simp reorient: ennreal_0)
     then have "(\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0"
       by (simp add: tendsto_norm_zero_iff)
   }
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -4130,7 +4130,7 @@
     have "winding_number \<gamma> y \<in> \<int>"  "winding_number \<gamma> z \<in>  \<int>"
       using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> S\<close> by auto
     with ne show ?thesis
-      by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
+      by (auto simp: Ints_def reorient: of_int_diff)
   qed
   have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
     using continuous_on_winding_number [OF \<gamma>] sg
@@ -6663,7 +6663,7 @@
       by (rule derivative_eq_intros | simp)+
     have y_le: "\<lbrakk>cmod (z - y) * 2 < r - cmod z\<rbrakk> \<Longrightarrow> cmod y \<le> cmod (of_real r + of_real (cmod z)) / 2" for z y
       using \<open>r > 0\<close>
-      apply (auto simp: algebra_simps norm_mult norm_divide norm_power of_real_add [symmetric] simp del: of_real_add)
+      apply (auto simp: algebra_simps norm_mult norm_divide norm_power reorient: of_real_add)
       using norm_triangle_ineq2 [of y z]
       apply (simp only: diff_le_eq norm_minus_commute mult_2)
       done
@@ -6671,7 +6671,7 @@
       using assms \<open>r > 0\<close> by simp
     moreover have "\<And>z. cmod z < r \<Longrightarrow> cmod ((of_real r + of_real (cmod z)) / 2) < cmod (of_real r)"
       using \<open>r > 0\<close>
-      by (simp add: of_real_add [symmetric] del: of_real_add)
+      by (simp reorient: of_real_add)
     ultimately have sum: "\<And>z. cmod z < r \<Longrightarrow> summable (\<lambda>n. of_real (cmod (a n)) * ((of_real r + complex_of_real (cmod z)) / 2) ^ n)"
       by (rule power_series_conv_imp_absconv_weak)
     have "\<exists>g g'. \<forall>z \<in> ball 0 r. (\<lambda>n.  (a n) * z ^ n) sums g z \<and>
@@ -6719,7 +6719,7 @@
       then have "0 \<le> r"
         by (meson less_eq_real_def norm_ge_zero order_trans)
       show ?thesis
-        using w by (simp add: dist_norm \<open>0\<le>r\<close> of_real_add [symmetric] del: of_real_add)
+        using w by (simp add: dist_norm \<open>0\<le>r\<close> reorient: of_real_add)
     qed
     have sum: "summable (\<lambda>n. a n * of_real (((cmod (z - w) + r) / 2) ^ n))"
       using assms [OF inb] by (force simp add: summable_def dist_norm)
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -1273,8 +1273,7 @@
       proof (rule add_mono)
         have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))"
           by (simp add: lmeasure_integral [OF meas_t]
-                        integral_mult_right [symmetric] integral_mult_left [symmetric]
-                   del: integral_mult_right integral_mult_left)
+                   reorient: integral_mult_right integral_mult_left)
         also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x.  (abs (det (matrix (f' x))))))"
         proof (rule sum_mono)
           fix k
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -244,7 +244,7 @@
       finally have "?\<mu> E - 2*e \<le> ?\<mu> (E - (E \<inter> \<Union>(snd`(p - s))))"
         using \<open>0 < e\<close> \<open>E \<in> sets ?L\<close> tagged_division_ofD(1)[OF p(1)]
         by (subst emeasure_Diff)
-           (auto simp: ennreal_plus[symmetric] top_unique simp del: ennreal_plus
+           (auto simp: top_unique reorient: ennreal_plus
                  intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
       also have "\<dots> \<le> ?\<mu> (\<Union>x\<in>p \<inter> s. snd x)"
       proof (safe intro!: emeasure_mono subsetI)
@@ -481,7 +481,7 @@
     by (simp add: nn_integral_add)
   with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
     by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
-       (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
+       (auto simp: add_top nn_integral_add top_add reorient: ennreal_plus)
   with add show ?case
     by (auto intro!: has_integral_add)
 next
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -271,7 +271,7 @@
 lemma fps_conv_radius_uminus [simp]:
   "fps_conv_radius (-f) = fps_conv_radius f"
   using fps_conv_radius_cmult_left[of "-1" f]
-  by (simp add: fps_const_neg [symmetric] del: fps_const_neg)
+  by (simp reorient: fps_const_neg)
 
 lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
   unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"]
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -1149,7 +1149,7 @@
 
 lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
   by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff
-        of_nat_Suc [symmetric] del: of_nat_Suc)
+        reorient: of_nat_Suc)
 
 lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
   by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc,
@@ -2430,7 +2430,7 @@
           inverse ((- 1) ^ n * fact n :: 'a)"
     by (intro tendsto_intros rGamma_zeros) simp_all
   also have "inverse ((- 1) ^ n * fact n) = ?c"
-    by (simp_all add: field_simps power_mult_distrib [symmetric] del: power_mult_distrib)
+    by (simp_all add: field_simps reorient: power_mult_distrib)
   finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" .
 qed
 
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -784,13 +784,13 @@
   fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
   assumes "f integrable_on s"
   shows "(\<lambda>x. f x / of_real c) integrable_on s"
-by (simp add: integrable_on_cmult_right divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+by (simp add: integrable_on_cmult_right divide_inverse assms reorient: of_real_inverse)
 
 lemma integrable_on_cdivide_iff [simp]:
   fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
   assumes "c \<noteq> 0"
   shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
-by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+by (simp add: divide_inverse assms reorient: of_real_inverse)
 
 lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
   unfolding has_integral_cbox
@@ -3431,7 +3431,7 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis using False
       by (simp add: image_affinity_cbox content_cbox'
-        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left del: prod_constant)
+        prod.distrib[symmetric] inner_diff_left reorient: prod_constant)
   qed
 qed
 
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -109,8 +109,7 @@
   from ereal_incseq_approx[OF this] guess X .
   then show thesis
     apply (intro that[of "\<lambda>i. - X i"])
-    apply (auto simp add: uminus_ereal.simps[symmetric] decseq_def incseq_def
-                simp del: uminus_ereal.simps)
+    apply (auto simp add: decseq_def incseq_def reorient: uminus_ereal.simps)
     apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
     done
 qed
@@ -143,7 +142,7 @@
     fix x i assume "l i \<le> x" "x \<le> u i"
     with \<open>a < ereal (l i)\<close> \<open>ereal (u i) < b\<close>
     show "a < ereal x" "ereal x < b"
-      by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric])
+      by (auto reorient: ereal_less_eq(3))
   qed
   show thesis
     by (intro that) fact+
@@ -304,8 +303,8 @@
   have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
     unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
     apply (rule Bochner_Integration.integral_cong [OF refl])
-    by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less uminus_ereal.simps[symmetric]
-             simp del: uminus_ereal.simps
+    by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
+             reorient: uminus_ereal.simps
              split: split_indicator)
   then show ?case
     unfolding interval_lebesgue_integral_def 
@@ -676,7 +675,7 @@
     fix i show "set_integrable lborel {l i .. u i} f"
       using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
       by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
-         (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
+         (auto reorient: ereal_less_eq)
   qed
   have 2: "set_borel_measurable lborel (einterval a b) f"
     unfolding set_borel_measurable_def
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -283,7 +283,7 @@
     also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
       using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
     finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
-      using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
+      using egt0 by (simp add: sum_nonneg reorient: ennreal_plus)
     then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
       by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal)
   qed
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -1622,7 +1622,7 @@
     using emeasure_subadditive[OF measurable] fin
     apply simp
     apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
-    apply (auto simp add: ennreal_plus[symmetric] simp del: ennreal_plus)
+    apply (auto reorient: ennreal_plus)
     done
 qed
 
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Regularity.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -107,7 +107,7 @@
     finally have "measure M (space M) \<le> measure M K + e"
       using \<open>0 < e\<close> by simp
     hence "emeasure M (space M) \<le> emeasure M K + e"
-      using \<open>0 < e\<close> by (simp add: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] del: ennreal_plus)
+      using \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
     moreover have "compact K"
       unfolding compact_eq_totally_bounded
     proof safe
@@ -139,9 +139,9 @@
       also have "\<dots> \<le> measure M (space M) - measure M K"
         by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
       also have "\<dots> \<le> e"
-        using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure ennreal_plus[symmetric] measure_nonneg del: ennreal_plus)
+        using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
       finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ennreal e"
-        using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps ennreal_plus[symmetric] measure_nonneg del: ennreal_plus)
+        using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps reorient: ennreal_plus)
       moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using \<open>closed A\<close> \<open>compact K\<close> by auto
       ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ennreal e"
         by blast
@@ -301,7 +301,7 @@
       have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (D i)) + e/2" using n0 by simp
       also have "(\<Sum>i<n0. measure M (D i)) \<le> (\<Sum>i<n0. measure M (K i) + e/(2*Suc n0))"
         using K \<open>0 < e\<close>
-        by (auto intro: sum_mono simp: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] simp del: ennreal_plus)
+        by (auto intro: sum_mono simp: emeasure_eq_measure reorient: ennreal_plus)
       also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))"
         by (simp add: sum.distrib)
       also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) +  e / 2" using \<open>0 < e\<close>
@@ -310,7 +310,7 @@
       have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2"
         by auto
       hence "M (\<Union>i. D i) < M ?K + e"
-        using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure measure_nonneg sum_nonneg ennreal_less_iff ennreal_plus[symmetric] simp del: ennreal_plus)
+        using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff reorient: ennreal_plus)
       moreover
       have "?K \<subseteq> (\<Union>i. D i)" using K by auto
       moreover
@@ -332,9 +332,9 @@
         from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this]
         show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
           using \<open>0<e\<close>
-          by (auto simp: emeasure_eq_measure measure_nonneg sum_nonneg ennreal_less_iff ennreal_plus[symmetric] ennreal_minus
+          by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus
                          finite_measure_mono sb
-                   simp del: ennreal_plus)
+                   reorient: ennreal_plus)
       qed
       then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
         "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
@@ -367,7 +367,7 @@
       also have "\<dots> = ennreal e"
         by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto
       finally have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ennreal e"
-        using \<open>0<e\<close> by (simp add: emeasure_eq_measure ennreal_plus[symmetric] measure_nonneg del: ennreal_plus)
+        using \<open>0<e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
       moreover
       have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
       moreover
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -869,7 +869,7 @@
     2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)" by simp
 
   have le: "ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))" for n x
-    by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_plus[symmetric] ennreal_minus del: ennreal_plus)
+    by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus reorient: ennreal_plus)
   then have le2: "(\<integral>\<^sup>+ x. ennreal (norm (F n x - f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) \<partial>M)" for n
     by (rule nn_integral_mono)
 
@@ -882,7 +882,7 @@
   proof (intro arg_cong[where f=liminf] ext)
     fix n
     have "\<And>x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))"
-      unfolding G_def by (simp add: ennreal_plus[symmetric] ennreal_minus del: ennreal_plus)
+      unfolding G_def by (simp add: ennreal_minus reorient: ennreal_plus)
     moreover have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \<partial>M)
             = (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)"
     proof (rule nn_integral_diff)
diff -r d45b78cb86cf -r 6aba668aea78 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -2085,7 +2085,7 @@
   have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
     using * by auto
   with * show "sets ?VV = sets ?V"
-    by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps)
+    by (simp add: sets_vimage_algebra2 vimage_comp comp_def reorient: ex_simps)
 qed (simp add: vimage_algebra_def emeasure_sigma)
 
 subsubsection \<open>Restricted Space Sigma Algebra\<close>
diff -r d45b78cb86cf -r 6aba668aea78 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Apr 26 19:51:32 2018 +0200
@@ -90,6 +90,7 @@
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
+  val reorient_simp: thm -> Proof.context -> Proof.context
   val init_simpset: thm list -> Proof.context -> Proof.context
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
@@ -560,16 +561,21 @@
     else rrule_eq_True ctxt thm name lhs elhs rhs thm
   end;
 
-fun extract_rews ctxt thms =
-  let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt
-  in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms end;
+fun extract_rews ctxt sym thms =
+  let
+    val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt;
+    val mk =
+      if sym then fn ctxt => fn th => (mk ctxt th) RL [Drule.symmetric_thm]
+      else mk  
+  in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms
+  end;
 
 fun extract_safe_rrules ctxt thm =
-  maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
+  maps (orient_rrule ctxt) (extract_rews ctxt false [thm]);
 
 fun mk_rrules ctxt thms =
   let
-    val rews = extract_rews ctxt thms
+    val rews = extract_rews ctxt false thms
     val raw_rrules = flat (map (mk_rrule ctxt) rews)
   in map mk_rrule2 raw_rrules end
 
@@ -578,20 +584,24 @@
 
 local
 
-fun comb_simps ctxt comb mk_rrule thms =
-  let val rews = extract_rews ctxt (map (Thm.transfer' ctxt) thms);
+fun comb_simps ctxt comb mk_rrule sym thms =
+  let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
   in fold (fold comb o mk_rrule) rews ctxt end;
 
 in
 
 fun ctxt addsimps thms =
-  comb_simps ctxt insert_rrule (mk_rrule ctxt) thms;
+  comb_simps ctxt insert_rrule (mk_rrule ctxt) false thms;
+
+fun addsymsimps ctxt thms =
+  comb_simps ctxt insert_rrule (mk_rrule ctxt) true thms;
 
 fun ctxt delsimps thms =
-  comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) thms;
+  comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) false thms;
 
 fun add_simp thm ctxt = ctxt addsimps [thm];
 fun del_simp thm ctxt = ctxt delsimps [thm];
+fun reorient_simp thm ctxt = addsymsimps (ctxt delsimps [thm]) [thm];
 
 end;
 
diff -r d45b78cb86cf -r 6aba668aea78 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/Pure/simplifier.ML	Thu Apr 26 19:51:32 2018 +0200
@@ -32,6 +32,7 @@
   val attrib: (thm -> Proof.context -> Proof.context) -> attribute
   val simp_add: attribute
   val simp_del: attribute
+  val simp_reorient: attribute
   val cong_add: attribute
   val cong_del: attribute
   val check_simproc: Proof.context -> xstring * Position.T -> string
@@ -89,6 +90,7 @@
 
 val simp_add = attrib add_simp;
 val simp_del = attrib del_simp;
+val simp_reorient = attrib reorient_simp;
 val cong_add = attrib add_cong;
 val cong_del = attrib del_cong;
 
@@ -267,6 +269,7 @@
 (* add / del *)
 
 val simpN = "simp";
+val reorientN = "reorient"
 val congN = "cong";
 val onlyN = "only";
 val no_asmN = "no_asm";
@@ -340,6 +343,7 @@
  [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;
@@ -347,6 +351,7 @@
 val simp_modifiers' =
  [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
   Args.$$$ onlyN -- Args.colon >>
     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;