# HG changeset patch
# User nipkow
# Date 1585662675 -7200
# Node ID 07bec530f02e36defc2644008c8a9d9ae5a80187
# Parent  2e8f861d21d428562022bec7498b0a54f09279b2
cleaned proofs

diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -158,7 +158,7 @@
   by (simp add: contractible_imp_path_connected_space)
 
 lemma connected_Euclidean_space: "connected_space (Euclidean_space n)"
-  by (simp add: contractible_Euclidean_space contractible_imp_connected_space)
+  by (simp add: contractible_imp_connected_space)
 
 lemma locally_path_connected_Euclidean_space:
    "locally_path_connected_space (Euclidean_space n)"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -2383,12 +2383,6 @@
     by (simp add: closed_map_id continuous_closed_imp_quotient_map)
 qed
 
-lemma homeomorphic_maps_i [simp]:"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
-  by (metis (full_types) eq_id_iff homeomorphic_maps_id)
-
-lemma homeomorphic_map_i [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
-  by (metis (no_types) eq_id_iff homeomorphic_map_id)
-
 lemma homeomorphic_map_compose:
   assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g"
   shows "homeomorphic_map X X'' (g \<circ> f)"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1789,13 +1789,13 @@
             have "False" if "\<xi> \<in> F n" "u < \<xi>" "\<xi> < v" for \<xi>
             proof -
               have "\<xi> \<notin> {z..v}"
-                by (metis DiffI disjoint_iff_not_equal less_irrefl singletonD that v(3))
+                by (metis DiffI disjoint_iff_not_equal less_irrefl singletonD that(1,3) v(3))
               moreover have "\<xi> \<notin> {w..z} \<inter> F n"
                 by (metis equals0D wzF_null)
               ultimately have "\<xi> \<in> {u..w}"
                 using that by auto
               then show ?thesis
-                by (metis DiffI disjoint_iff_not_equal less_eq_real_def not_le singletonD that u(3))
+                by (metis DiffI disjoint_iff_not_equal less_eq_real_def not_le singletonD that(1,2) u(3))
             qed
             moreover
             have "\<lbrakk>\<xi> \<in> F n; v < \<xi>; \<xi> < u\<rbrakk> \<Longrightarrow> False" for \<xi>
@@ -1811,7 +1811,7 @@
           by (metis dist_norm dist_triangle_half_r less_irrefl)
       qed (auto simp: open_segment_commute)
       show ?thesis
-        unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that F01 subsetCE pqF)
+        unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
     qed
     show "closed {0..1::real}" by auto
   qed (meson \<phi>_def)
@@ -1972,7 +1972,7 @@
     show "pathstart (subpath u v g) = a" "pathfinish (subpath u v g) = b"
       by (simp_all add: \<open>a = g u\<close> \<open>b = g v\<close>)
     show "path_image (subpath u v g) \<subseteq> path_image p"
-      by (metis \<open>arc g\<close> \<open>u \<in> {0..1}\<close> \<open>v \<in> {0..1}\<close> arc_imp_path order_trans pag path_image_def path_image_subpath_subset ph)
+      by (metis \<open>u \<in> {0..1}\<close> \<open>v \<in> {0..1}\<close> order_trans pag path_image_def path_image_subpath_subset ph)
     show "arc (subpath u v g)"
       using \<open>arc g\<close> \<open>a = g u\<close> \<open>b = g v\<close> \<open>u \<in> {0..1}\<close> \<open>v \<in> {0..1}\<close> arc_subpath_arc \<open>a \<noteq> b\<close> by blast
   qed
@@ -2049,7 +2049,7 @@
                                  and g: "pathstart g = y" "pathfinish g = z"
     using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise)
   have "compact (g -` frontier S \<inter> {0..1})"
-    apply (simp add: compact_eq_bounded_closed bounded_Int bounded_closed_interval)
+    apply (simp add: compact_eq_bounded_closed bounded_Int)
      apply (rule closed_vimage_Int)
     using \<open>arc g\<close> apply (auto simp: arc_def path_def)
     done
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Ball_Volume.thy
--- a/src/HOL/Analysis/Ball_Volume.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Ball_Volume.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -46,7 +46,7 @@
        (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
   also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
     by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
-       (auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult' mult_ac)
+       (auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult')
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
                     (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
     (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add)
@@ -137,7 +137,7 @@
       proof (cases "y \<in> {-r<..<r}")
         case True
         hence "y\<^sup>2 < r\<^sup>2" by (subst real_sqrt_less_iff [symmetric]) auto
-        thus ?thesis by (subst insert.IH) (auto simp: real_sqrt_less_iff)
+        thus ?thesis by (subst insert.IH) (auto)
       qed (insert elim, auto)
     qed
   qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -403,7 +403,7 @@
   from g have "simple_bochner_integral M (\<lambda>x. f (g x)) =
     (\<Sum>y\<in>g ` space M. measure M {x \<in> space M. g x = y} *\<^sub>R f y)"
     by (intro simple_bochner_integral_partition)
-       (auto simp: simple_bochner_integrable_compose2[where p="\<lambda>x y. f x"] zero
+       (auto simp: simple_bochner_integrable_compose2[where p="\<lambda>x y. f x"]
              elim: simple_bochner_integrable.cases)
   also have "\<dots> = f (simple_bochner_integral M g)"
     by (simp add: simple_bochner_integral_def sum scale)
@@ -1379,7 +1379,7 @@
 lemma integral_minus_iff[simp]:
   "integrable M (\<lambda>x. - f x ::'a::{banach, second_countable_topology}) \<longleftrightarrow> integrable M f"
   unfolding integrable_iff_bounded
-  by (auto intro: borel_measurable_uminus[of "\<lambda>x. - f x" M, simplified])
+  by (auto)
 
 lemma integrable_indicator_iff:
   "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
@@ -1634,7 +1634,7 @@
       with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
         by auto
     qed
-  qed (auto simp: integrable_mult_left_iff)
+  qed (auto)
   also have "\<dots> = integral\<^sup>L M f"
     using nonneg by (auto intro!: integral_cong_AE)
   finally show ?thesis .
@@ -1657,7 +1657,7 @@
         by (simp add: integrable_indicator_iff ennreal_indicator emeasure_eq_ennreal_measure)
     next
       case (mult f c) then show ?case
-        by (auto simp add: integrable_mult_left_iff nn_integral_cmult ennreal_mult integral_nonneg_AE)
+        by (auto simp add: nn_integral_cmult ennreal_mult integral_nonneg_AE)
     next
       case (add g f)
       then have "integrable M f" "integrable M g"
@@ -2756,7 +2756,7 @@
       by (auto split: split_indicator simp: eq_commute[of x] cong: conj_cong)
   qed
   also have "\<dots> = (\<Sum>a\<in>A. f a * measure M {a})"
-    using finite by (subst integral_sum) (auto simp add: integrable_mult_left_iff)
+    using finite by (subst integral_sum) (auto)
   finally show ?thesis .
 qed
 
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1758,7 +1758,7 @@
       also have "\<dots> < ?I i / 2 + ?I i / 2"
         by (intro add_strict_mono d less_trans[OF _ j] *)
       also have "\<dots> \<le> ?I i"
-        by (simp add: field_simps of_nat_Suc)
+        by (simp add: field_simps)
       finally show "dist (f y) (f z) \<le> ?I i"
         by simp
     qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1436,7 +1436,7 @@
       using idplus [OF \<open>m \<noteq> n\<close>] by simp
   qed
   then show ?thesis
-    by (metis \<open>linear f\<close> matrix_vector_mul)
+    by (metis \<open>linear f\<close> matrix_vector_mul(2))
 qed
 
 end
\ No newline at end of file
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -543,7 +543,7 @@
                 also have "\<dots> = norm (f' x (y - x) - (f y - f x)) / r"
                   using \<open>r > 0\<close> by (simp add: divide_simps scale_right_diff_distrib [symmetric])
                 also have "\<dots> \<le> norm (f y - (f x + f' x (y - x))) / norm (y - x)"
-                  using that \<open>r > 0\<close> False by (simp add: algebra_simps field_split_simps dist_norm norm_minus_commute mult_right_mono)
+                  using that \<open>r > 0\<close> False by (simp add: field_split_simps dist_norm norm_minus_commute mult_right_mono)
                 also have "\<dots> < k"
                   using that \<open>0 < \<zeta>\<close> by (simp add: dist_commute r_def  \<zeta> [OF \<open>y \<in> S\<close> False])
                 finally show "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) < k" .
@@ -1656,7 +1656,7 @@
             show "linear ((*v) (matrix (f' x) - B))"
               by (rule matrix_vector_mul_linear)
             have "((\<lambda>y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
-              using tendsto_minus [OF lim_df] by (simp add: algebra_simps field_split_simps)
+              using tendsto_minus [OF lim_df] by (simp add: field_split_simps)
             then show "((\<lambda>y. (matrix (f' x) - B) *v (y - x) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
             proof (rule Lim_transform)
               have "((\<lambda>y. ((f y + B *v x - (f x + B *v y)) /\<^sub>R norm (y - x))) \<longlongrightarrow> 0) (at x within S)"
@@ -1724,7 +1724,7 @@
               then show "((\<lambda>y. (matrix (f' x) - B) *v (y - x) /\<^sub>R
                            norm (y - x) - (f x + f' x (y - x) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0)
                           (at x within S)"
-                by (simp add: algebra_simps diff lin_df matrix_vector_mul_linear scalar_mult_eq_scaleR)
+                by (simp add: algebra_simps diff lin_df scalar_mult_eq_scaleR)
             qed
           qed (use x in \<open>simp; auto simp: not_less\<close>)
           ultimately have "f' x = (*v) B"
@@ -2168,7 +2168,7 @@
         proof (rule order_trans [OF measT])
           have "?DVU = (d * 2 * (4 * B) ^ (?n - 1)) * norm (v - u)^?n"
             using \<open>c > 0\<close>
-            apply (simp add: algebra_simps power_mult_distrib)
+            apply (simp add: algebra_simps)
             by (metis Suc_pred power_Suc zero_less_card_finite)
           also have "\<dots> \<le> (e / (2*c) ^ ?m / (?m ^ ?m)) * norm(v - u) ^ ?n"
             by (rule mult_right_mono [OF d]) auto
@@ -2239,7 +2239,7 @@
           using \<open>c > 0\<close> by (simp add: content_cbox_if_cart)
         finally have "sum ?\<mu> \<F> \<le> (2 ^ ?m * c ^ ?m)" .
         then show ?thesis
-          using \<open>e > 0\<close> \<open>c > 0\<close> by (auto simp: field_split_simps mult_less_0_iff)
+          using \<open>e > 0\<close> \<open>c > 0\<close> by (auto simp: field_split_simps)
       qed
       finally show ?thesis .
     qed
@@ -2384,7 +2384,7 @@
         done
       ultimately show ?thesis
         using \<open>y > 0\<close> integral_restrict_Int [of S "{t. h n (g t) = y}" "\<lambda>t. \<bar>det (matrix (g' t))\<bar> * y"]
-        apply (simp add: integrable_on_indicator integrable_on_cmult_iff integral_indicator)
+        apply (simp add: integrable_on_indicator integral_indicator)
         apply (simp add: indicator_def if_distrib cong: if_cong)
         done
     qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -489,7 +489,7 @@
 
 lemma analytic_on_sum [analytic_intros]:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on S"
-  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
+  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_add)
 
 lemma deriv_left_inverse:
   assumes "f holomorphic_on S" and "g holomorphic_on T"
@@ -579,11 +579,11 @@
 
 lemma deriv_cmult_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
-by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
+by (auto simp: complex_derivative_mult_at)
 
 lemma deriv_cmult_right_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
-by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
+by (auto simp: complex_derivative_mult_at)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Complex differentiation of sequences and series\<close>
 
@@ -758,7 +758,7 @@
     apply (rule field_differentiable_bound
       [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
          and S = "closed_segment w z", OF convex_closed_segment])
-    apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs]
+    apply (auto simp: DERIV_subset [OF sum_deriv wzs]
                   norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
     done
   also have "...  \<le> B * norm (z - w) ^ Suc n / (fact n)"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -612,7 +612,7 @@
   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)
   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib sin_squared_eq)
-  apply (simp add: power2_eq_square algebra_simps field_split_simps)
+  apply (simp add: power2_eq_square field_split_simps)
   done
 
 lemma norm_sin_squared:
@@ -621,7 +621,7 @@
   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq)
-  apply (simp add: power2_eq_square algebra_simps field_split_simps)
+  apply (simp add: power2_eq_square field_split_simps)
   done
 
 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
@@ -1102,7 +1102,7 @@
   by auto
 
 lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
-  apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric] mult.commute)
+  apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric])
   by (metis of_real_power zero_less_norm_iff zero_less_power)
 
 lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)"
@@ -1946,7 +1946,7 @@
   by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)
 
 lemma Arg_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg (cnj z) = Arg (inverse z)"
-  apply (simp add: Arg_eq_iff field_split_simps complex_norm_square [symmetric] mult.commute)
+  apply (simp add: Arg_eq_iff field_split_simps complex_norm_square [symmetric])
   by (metis of_real_power zero_less_norm_iff zero_less_power)
 
 lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> then Arg z else - Arg z)"
@@ -2936,7 +2936,7 @@
     unfolding Arctan_def scaleR_conv_of_real
     apply (intro derivative_eq_intros | simp add: nz0 *)+
     using nz0 nz1 zz
-    apply (simp add: algebra_simps field_split_simps power2_eq_square)
+    apply (simp add: field_split_simps power2_eq_square)
     apply algebra
     done
 qed
@@ -3014,7 +3014,7 @@
   have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
   proof (rule has_field_derivative_zero_constant)
     fix u :: complex assume "u \<in> ball 0 1"
-    hence u: "norm u < 1" by (simp add: dist_0_norm)
+    hence u: "norm u < 1" by (simp)
     define K where "K = (norm u + 1) / 2"
     from u and abs_Im_le_cmod[of u] have Im_u: "\<bar>Im u\<bar> < 1" by linarith
     from u have K: "0 \<le> K" "norm u < K" "K < 1" by (simp_all add: K_def)
@@ -3634,7 +3634,7 @@
   assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
 proof -
   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
-    by (simp add: power_mult_distrib algebra_simps)
+    by (simp add: algebra_simps)
   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
   proof
     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
@@ -3665,7 +3665,7 @@
   assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
 proof -
   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
-    by (simp add: power_mult_distrib algebra_simps)
+    by (simp add: algebra_simps)
   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
   proof
     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
@@ -3971,7 +3971,7 @@
     shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
 proof -
   have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
-    by (simp add: of_real_numeral)
+    by (simp)
   then show ?thesis
     apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
     apply (simp only: * cos_of_real sin_of_real)
@@ -4006,7 +4006,7 @@
    note * = this
   show ?thesis
     using assms
-    by (simp add: exp_eq field_split_simps mult_ac of_real_numeral *)
+    by (simp add: exp_eq field_split_simps *)
 qed
 
 corollary bij_betw_roots_unity:
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -346,7 +346,7 @@
 proof-
   have "{a..b} = {a..} \<inter> {..b}" by auto
   also have "interior \<dots> = {a<..} \<inter> {..<b}"
-    by (simp add: interior_real_atLeast interior_real_atMost)
+    by (simp)
   also have "\<dots> = {a<..<b}" by auto
   finally show ?thesis .
 qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Cross3.thy
--- a/src/HOL/Analysis/Cross3.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Cross3.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -100,7 +100,7 @@
 
 lemma  cross_basis_nonzero:
   "u \<noteq> 0 \<Longrightarrow> u \<times> axis 1 1 \<noteq> 0 \<or> u \<times> axis 2 1 \<noteq> 0 \<or> u \<times> axis 3 1 \<noteq> 0"
-  by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
+  by (clarsimp simp add: axis_def cross3_simps) (metis exhaust_3)
 
 lemma  cross_dot_cancel:
   fixes x::"real^3"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1056,7 +1056,7 @@
       by (rule openE)
     then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
       by (intro has_derivative_zero_constant)
-         (auto simp: at_within_open[OF _ open_ball] f convex_ball)
+         (auto simp: at_within_open[OF _ open_ball] f)
     with \<open>0<e\<close> have "\<forall>x\<in>ball a e. f a = f x"
       by auto
     then show "eventually (\<lambda>b. f a = f b) (at a within s)"
@@ -2187,7 +2187,7 @@
   show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
       (at t within T)"
     by (rule Lim_transform_eventually)
-      (auto simp: algebra_simps field_split_simps exp_add_commuting[symmetric])
+      (auto simp: field_split_simps exp_add_commuting[symmetric])
 qed (rule bounded_linear_scaleR_left)
 
 lemma exp_times_scaleR_commute: "exp (t *\<^sub>R A) * A = A * exp (t *\<^sub>R A)"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -109,7 +109,7 @@
 qed
 
 lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
-  by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute)
+  by (simp add: open_dist subset_eq Ball_def dist_commute)
 
 lemma openI [intro?]: "(\<And>x. x\<in>S \<Longrightarrow> \<exists>e>0. ball x e \<subseteq> S) \<Longrightarrow> open S"
   by (auto simp: open_contains_ball)
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -798,7 +798,7 @@
 corollary cobounded_imp_unbounded:
     fixes S :: "'a::{real_normed_vector, perfect_space} set"
     shows "bounded (- S) \<Longrightarrow> \<not> bounded S"
-  using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
+  using bounded_Un [of S "-S"]  by (simp)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relations among convergence and absolute convergence for power series\<close>
 
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -251,7 +251,7 @@
   have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
     using f g by (auto simp: inj_on_def)
 
-  note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del]
+  note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del]
      ccSUP_insert[simp del]
   show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
     unfolding map_prod_def[symmetric]
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -3357,7 +3357,7 @@
   have eq: "?g =
         (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
                (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
-    by (simp add: sum.delta)
+    by (simp)
   have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
            (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
            absolutely_integrable_on S"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -742,7 +742,7 @@
       show "continuous_on UNIV (g \<circ> (\<theta> n))" for n :: nat
         unfolding \<theta>_def
         apply (intro continuous_on_compose2 [OF contg] continuous_intros conth)
-        apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj algebra_simps field_split_simps)
+        apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj field_split_simps)
         done
       show "(\<lambda>n. (g \<circ> \<theta> n) x) \<longlonglongrightarrow> g (f x)"
         if "x \<notin> N" for x
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -304,7 +304,7 @@
   fix P d
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
-    by (auto simp: zero_less_dist_iff dist_commute)
+    by (auto simp: dist_commute)
   then show "\<exists>r>0. Inf (f ` (Collect P)) \<le> Inf (f ` (S \<inter> ball x r - {x}))"
     by (intro exI[of _ d] INF_mono conjI \<open>0 < d\<close>) auto
 next
@@ -324,7 +324,7 @@
   fix P d
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
-    by (auto simp: zero_less_dist_iff dist_commute)
+    by (auto simp: dist_commute)
   then show "\<exists>r>0. Sup (f ` (S \<inter> ball x r - {x})) \<le> Sup (f ` (Collect P))"
     by (intro exI[of _ d] SUP_mono conjI \<open>0 < d\<close>) auto
 next
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -429,7 +429,7 @@
   have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))"
     by (rule exp_converges)
   also have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) = (\<lambda>n. norm (fps_nth (fps_exp c) n * z ^ n))"
-    by (rule ext) (simp add: norm_divide norm_mult norm_power field_split_simps power_mult_distrib)
+    by (rule ext) (simp add: norm_divide norm_mult norm_power field_split_simps)
   finally have "summable \<dots>" by (simp add: sums_iff)
   thus "summable (\<lambda>n. fps_nth (fps_exp c) n * z ^ n)"
     by (rule summable_norm_cancel)
@@ -585,7 +585,7 @@
 lemma eval_fps_exp [simp]:
   fixes c :: "'a :: {banach, real_normed_field}"
   shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def
-  by (simp add: eval_fps_def exp_def scaleR_conv_of_real field_split_simps power_mult_distrib)
+  by (simp add: eval_fps_def exp_def scaleR_conv_of_real field_split_simps)
 
 text \<open>
   The case of division is more complicated and will therefore not be handled here.
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -677,10 +677,10 @@
       path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
       path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
       path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
-      by(auto simp add: path_image_join path_linepath)
+      by(auto simp add: path_image_join)
   have abab: "cbox a b \<subseteq> cbox ?a ?b"
     unfolding interval_cbox_cart[symmetric]
-    by (auto simp add:less_eq_vec_def forall_2 vector_2)
+    by (auto simp add:less_eq_vec_def forall_2)
   obtain z where
     "z \<in> path_image
           (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Function_Metric.thy
--- a/src/HOL/Analysis/Function_Metric.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Function_Metric.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -187,7 +187,7 @@
     have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
       by (rule dist_fun_le_dist_first_terms)
     also have "... \<le> 2 * f + e / 8"
-      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps field_split_simps)
+      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: field_split_simps)
     also have "... \<le> e/2 + e/8"
       unfolding f_def by auto
     also have "... < e"
@@ -331,7 +331,7 @@
       also have "... < (1/2)^k * min e 1"
         using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
       finally have "min (dist (u m i) (u n i)) 1 < min e 1"
-        by (auto simp add: algebra_simps field_split_simps)
+        by (auto simp add: field_split_simps)
       then show "dist (u m i) (u n i) < e" by auto
     qed
     then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
@@ -371,7 +371,7 @@
         using dist_fun_le_dist_first_terms by auto
       also have "... \<le> 2 * e/4 + e/4"
         apply (rule add_mono)
-        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps field_split_simps)
+        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: field_split_simps)
       also have "... < e" by auto
       finally show ?thesis by simp
     qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -198,7 +198,7 @@
   have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
     using openin_topspace not_finite_existsD by auto
   then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
-    unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
+    unfolding product_topology_def using PiE_def by (auto)
 qed
 
 lemma product_topology_basis:
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -3682,7 +3682,7 @@
       qed
       show "disjoint \<V>"
         apply (clarsimp simp add: \<V>_def pairwise_def disjnt_def add.commute [of _ "x*y" for x y]
-                        image_add_ball ball_eq_ball_iff)
+                        ball_eq_ball_iff)
         apply (rule disjoint_ballI)
         apply (auto simp: dist_norm neq_iff)
         by (metis norm_minus_commute xy)+
@@ -5321,7 +5321,7 @@
   assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
   apply (rule connected_frontier_simple)
   using C in_components_connected apply blast
-  by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
+  by (metis assms component_complement_connected)
 
 lemma connected_frontier_disjoint:
   fixes S :: "'a :: euclidean_space set"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -395,7 +395,7 @@
     from d have "\<lceil>2 * (cmod z + d)\<rceil> \<ge> \<lceil>0::real\<rceil>"
       by (intro ceiling_mono mult_nonneg_nonneg add_nonneg_nonneg) simp_all
     hence "2 * (norm z + d) \<le> of_nat (nat \<lceil>2 * (norm z + d)\<rceil>)" unfolding N_def
-      by (simp_all add: le_of_int_ceiling)
+      by (simp_all)
     also have "... \<le> of_nat N" unfolding N_def
       by (subst of_nat_le_iff) (rule max.coboundedI2, rule max.cobounded1)
     finally have "of_nat N \<ge> 2 * (norm z + d)" .
@@ -540,7 +540,7 @@
     also have "\<dots> = z * of_real (harm n) - (\<Sum>k=1..n. ln (1 + z / of_nat k))"
       by (simp add: harm_def sum_subtractf sum_distrib_left divide_inverse)
     also from n have "\<dots> - ?g n = 0"
-      by (simp add: ln_Gamma_series_def sum_subtractf algebra_simps Ln_of_nat)
+      by (simp add: ln_Gamma_series_def sum_subtractf algebra_simps)
     finally show "(\<Sum>k<n. ?f k) - ?g n = 0" .
   qed
   show "(\<lambda>n. (\<Sum>k<n. ?f k) - ?g n) \<longlonglongrightarrow> 0" by (subst tendsto_cong[OF A]) simp_all
@@ -583,7 +583,7 @@
     with t_nz have "?f n t = 1 / (of_nat (Suc n) * (1 + of_nat (Suc n)/t))"
       by (simp add: field_split_simps eq_neg_iff_add_eq_0 del: of_nat_Suc)
     also have "norm \<dots> = inverse (of_nat (Suc n)) * inverse (norm (of_nat (Suc n)/t + 1))"
-      by (simp add: norm_divide norm_mult field_split_simps add_ac del: of_nat_Suc)
+      by (simp add: norm_divide norm_mult field_split_simps del: of_nat_Suc)
     also {
       from z t_nz ball[OF t] have "of_nat (Suc n) / (4 * norm z) \<le> of_nat (Suc n) / (2 * norm t)"
         by (intro divide_left_mono mult_pos_pos) simp_all
@@ -1110,7 +1110,7 @@
              pochhammer z (Suc (Suc n)) / (fact n * exp (z * of_real (ln (of_nat n))))"
       by (subst pochhammer_rec) (simp add: rGamma_series_def field_simps exp_add exp_of_real)
     also from n have "\<dots> = ?f n * rGamma_series z n"
-      by (subst pochhammer_rec') (simp_all add: field_split_simps rGamma_series_def add_ac)
+      by (subst pochhammer_rec') (simp_all add: field_split_simps rGamma_series_def)
     finally show "?f n * rGamma_series z n = z * rGamma_series (z + 1) n" ..
   qed
   moreover have "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> ((z+1) * 0 + 1) * rGamma z"
@@ -1175,7 +1175,7 @@
   have "1/2 > (0::real)" by simp
   from tendstoD[OF assms, OF this]
     show "eventually (\<lambda>n. g n / Gamma_series z n * Gamma_series z n = g n) sequentially"
-    by (force elim!: eventually_mono simp: dist_real_def dist_0_norm)
+    by (force elim!: eventually_mono simp: dist_real_def)
   from assms have "(\<lambda>n. g n / Gamma_series z n * Gamma_series z n) \<longlonglongrightarrow> 1 * Gamma z"
     by (intro tendsto_intros)
   thus "(\<lambda>n. g n / Gamma_series z n * Gamma_series z n) \<longlonglongrightarrow> Gamma z" by simp
@@ -1189,7 +1189,7 @@
 proof (rule Lim_transform_eventually)
   have "1/2 > (0::real)" by simp
   from tendstoD[OF assms(2), OF this] show "eventually (\<lambda>n. g n * f n / f n = g n) sequentially"
-    by (force elim!: eventually_mono simp: dist_real_def dist_0_norm)
+    by (force elim!: eventually_mono simp: dist_real_def)
   from assms have "(\<lambda>n. g n * f n / f n) \<longlonglongrightarrow> 1 / rGamma z"
     by (intro tendsto_divide assms) (simp_all add: rGamma_eq_zero_iff)
   thus "(\<lambda>n. g n * f n / f n) \<longlonglongrightarrow> Gamma z" by (simp add: Gamma_def divide_inverse)
@@ -1409,13 +1409,13 @@
                        \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma z +
               rGamma z * d * (y - z)) /\<^sub>R  cmod (y - z)) \<midarrow>z\<rightarrow> 0"
       by (simp add: has_field_derivative_def has_derivative_def Digamma_def sums_def [abs_def]
-                    netlimit_at of_real_def[symmetric] suminf_def)
+                    of_real_def[symmetric] suminf_def)
 next
   fix n :: nat
   from has_field_derivative_rGamma_complex_nonpos_Int[of n]
   show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * prod of_nat {1..n} *
                   (y - z)) /\<^sub>R cmod (y - z)) \<midarrow>z\<rightarrow> 0"
-    by (simp add: has_field_derivative_def has_derivative_def fact_prod netlimit_at Let_def)
+    by (simp add: has_field_derivative_def has_derivative_def fact_prod Let_def)
 next
   fix z :: complex
   from rGamma_series_complex_converges[of z] have "rGamma_series z \<longlonglongrightarrow> rGamma z"
@@ -1535,7 +1535,7 @@
   fix n :: nat assume n: "n > 0"
   have "Re (rGamma_series (of_real x) n) =
           Re (of_real (pochhammer x (Suc n)) / (fact n * exp (of_real (x * ln (real_of_nat n)))))"
-    using n by (simp add: rGamma_series_def powr_def Ln_of_nat pochhammer_of_real)
+    using n by (simp add: rGamma_series_def powr_def pochhammer_of_real)
   also from n have "\<dots> = Re (of_real ((pochhammer x (Suc n)) /
                               (fact n * (exp (x * ln (real_of_nat n))))))"
     by (subst exp_of_real) simp
@@ -1569,7 +1569,7 @@
                        \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma x +
               rGamma x * d * (y - x)) /\<^sub>R  norm (y - x)) \<midarrow>x\<rightarrow> 0"
       by (simp add: has_field_derivative_def has_derivative_def Digamma_def sums_def [abs_def]
-                    netlimit_at of_real_def[symmetric] suminf_def)
+                    of_real_def[symmetric] suminf_def)
 next
   fix n :: nat
   have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))"
@@ -1577,7 +1577,7 @@
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
   thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * prod of_nat {1..n} *
                   (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
-    by (simp add: has_field_derivative_def has_derivative_def fact_prod netlimit_at Let_def)
+    by (simp add: has_field_derivative_def has_derivative_def fact_prod Let_def)
 next
   fix x :: real
   have "rGamma_series x \<longlonglongrightarrow> rGamma x"
@@ -1619,7 +1619,7 @@
   assume xn: "x > 0" "n > 0"
   have "Ln (complex_of_real x / of_nat k + 1) = of_real (ln (x / of_nat k + 1))" if "k \<ge> 1" for k
     using that xn by (subst Ln_of_real [symmetric]) (auto intro!: add_nonneg_pos simp: field_simps)
-  with xn show ?thesis by (simp add: ln_Gamma_series_def Ln_of_nat Ln_of_real)
+  with xn show ?thesis by (simp add: ln_Gamma_series_def Ln_of_real)
 qed
 
 lemma ln_Gamma_real_converges:
@@ -2061,7 +2061,7 @@
     by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all
   with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real)
   from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis
-    by (simp add: field_split_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
+    by (simp add: field_split_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real)
 qed
 
 text \<open>
@@ -2126,13 +2126,13 @@
 
   have h_eq: "h t = h2 t" if "abs (Re t) < 1" for t
   proof -
-    from that have t: "t \<in> \<int> \<longleftrightarrow> t = 0" by (auto elim!: Ints_cases simp: dist_0_norm)
+    from that have t: "t \<in> \<int> \<longleftrightarrow> t = 0" by (auto elim!: Ints_cases)
     hence "h t = a*cot (a*t) - 1/t + Digamma (1 + t) - Digamma (1 - t)"
       unfolding h_def using Digamma_plus1[of t] by (force simp: field_simps a_def)
     also have "a*cot (a*t) - 1/t = (F t) / (G t)"
       using t by (auto simp add: divide_simps sin_eq_0 cot_def a_def F_def G_def)
     also have "\<dots> = (\<Sum>n. f n * (a*t)^n) / (\<Sum>n. g n * (a*t)^n)"
-      using sums[of t] that by (simp add: sums_iff dist_0_norm)
+      using sums[of t] that by (simp add: sums_iff)
     finally show "h t = h2 t" by (simp only: h2_def)
   qed
 
@@ -2167,7 +2167,7 @@
     have d: "abs (Re d) < 1" "norm z < norm d" by (simp_all add: d_def norm_mult del: of_real_add)
     have "eventually (\<lambda>z. h z = h2 z) (nhds z)"
       using eventually_nhds_in_nhd[of z ?A] using h_eq z
-      by (auto elim!: eventually_mono simp: dist_0_norm)
+      by (auto elim!: eventually_mono)
 
     moreover from sums(2)[OF z] z have nz: "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0"
       unfolding G_def by (auto simp: sums_iff sin_eq_0 a_def)
@@ -2326,7 +2326,7 @@
         show "g z = of_real pi * Gamma (1 + z) * Gamma (1 - z) * ?t z"
         proof (cases "z = 0")
           assume z': "z \<noteq> 0"
-          with z have z'': "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z \<notin> \<int>" by (auto elim!: Ints_cases simp: dist_0_norm)
+          with z have z'': "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z \<notin> \<int>" by (auto elim!: Ints_cases)
           from Gamma_plus1[OF this(1)] have "Gamma z = Gamma (z + 1) / z" by simp
           with z'' z' show ?thesis by (simp add: g_def ac_simps)
         qed (simp add: g_def)
@@ -2471,7 +2471,7 @@
       show "\<forall>z\<in>B. norm (h' z) \<le> M/2"
       proof
         fix t :: complex assume t: "t \<in> B"
-        from h'_eq[of t] t have "h' t = (h' (t/2) + h' ((t+1)/2)) / 4" by (simp add: dist_0_norm)
+        from h'_eq[of t] t have "h' t = (h' (t/2) + h' ((t+1)/2)) / 4" by (simp)
         also have "norm \<dots> = norm (h' (t/2) + h' ((t+1)/2)) / 4" by simp
         also have "norm (h' (t/2) + h' ((t+1)/2)) \<le> norm (h' (t/2)) + norm (h' ((t+1)/2))"
           by (rule norm_triangle_ineq)
@@ -2482,7 +2482,7 @@
         also have "(M + M) / 4 = M / 2" by simp
         finally show "norm (h' t) \<le> M/2" by - simp_all
       qed
-    qed (insert bdd, auto simp: cball_eq_empty)
+    qed (insert bdd, auto)
     hence "M \<le> 0" by simp
     finally show "h' z = 0" by simp
   qed
@@ -2512,7 +2512,7 @@
   with c have A: "h z * g z = 0" for z by simp
   hence "(g has_field_derivative 0) (at z)" for z using g_g'[of z] by simp
   hence "\<exists>c'. \<forall>z\<in>UNIV. g z = c'" by (intro has_field_derivative_zero_constant) simp_all
-  then obtain c' where c: "\<And>z. g z = c'" by (force simp: dist_0_norm)
+  then obtain c' where c: "\<And>z. g z = c'" by (force)
   from this[of 0] have "c' = pi" unfolding g_def by simp
   with c have "g z = pi" by simp
 
@@ -2547,7 +2547,7 @@
 
 lemma Gamma_reflection_complex':
   "Gamma z * Gamma (- z :: complex) = - of_real pi / (z * sin (of_real pi * z))"
-  using rGamma_reflection_complex'[of z] by (force simp add: Gamma_def field_split_simps mult_ac)
+  using rGamma_reflection_complex'[of z] by (force simp add: Gamma_def field_split_simps)
 
 
 
@@ -2675,7 +2675,7 @@
   from z have z': "z \<noteq> 0" by auto
 
   have "eventually (\<lambda>n. ?r' n = ?r n) sequentially"
-    using z by (auto simp: field_split_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
+    using z by (auto simp: field_split_simps Gamma_series_def ring_distribs exp_diff ln_div
                      intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
   moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
     by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
@@ -2819,7 +2819,7 @@
   have "(\<lambda>n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n))))
             \<longlonglongrightarrow> 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \<longlonglongrightarrow> _")
     using Gamma_gbinomial[of "of_nat k :: 'a"]
-    by (simp add: binomial_gbinomial add_ac Gamma_def field_split_simps exp_of_real [symmetric] exp_minus)
+    by (simp add: binomial_gbinomial Gamma_def field_split_simps exp_of_real [symmetric] exp_minus)
   also have "Gamma (of_nat (Suc k)) = fact k" by (simp add: Gamma_fact)
   finally show "?f \<longlonglongrightarrow> 1 / fact k" .
 
@@ -2862,7 +2862,7 @@
     next
       case False
       with \<open>z = 0\<close> show ?thesis
-        by (simp_all add: Beta_pole1 one_minus_of_nat_in_nonpos_Ints_iff gbinomial_1)
+        by (simp_all add: Beta_pole1 one_minus_of_nat_in_nonpos_Ints_iff)
     qed
   next
     case False
@@ -2885,7 +2885,7 @@
   have "(z gchoose n) = Gamma (z + 2) / (z + 1) / (fact n * Gamma (z - of_nat n + 1))"
     by (subst gbinomial_Beta[OF assms]) (simp_all add: Beta_def Gamma_fact [symmetric] add_ac)
   also from assms have "Gamma (z + 2) / (z + 1) = Gamma (z + 1)"
-    using Gamma_plus1[of "z+1"] by (auto simp add: field_split_simps mult_ac add_ac)
+    using Gamma_plus1[of "z+1"] by (auto simp add: field_split_simps)
   finally show ?thesis .
 qed
 
@@ -3073,7 +3073,7 @@
   have "eventually (\<lambda>n. Gamma_series z n =
           of_nat n powr z * fact n / pochhammer z (n+1)) sequentially"
     using eventually_gt_at_top[of "0::nat"]
-    by eventually_elim (simp add: powr_def algebra_simps Ln_of_nat Gamma_series_def)
+    by eventually_elim (simp add: powr_def algebra_simps Gamma_series_def)
   from this and Gamma_series_LIMSEQ[of z]
     have C: "(\<lambda>k. of_nat k powr z * fact k / pochhammer z (k+1)) \<longlonglongrightarrow> Gamma z"
     by (blast intro: Lim_transform_eventually)
@@ -3441,7 +3441,7 @@
       fix n :: nat and x :: real assume x: "x \<in> ball 0 1"
       {
         fix k :: nat assume k: "k \<ge> 1"
-        from x have "x^2 < 1" by (auto simp: dist_0_norm abs_square_less_1)
+        from x have "x^2 < 1" by (auto simp: abs_square_less_1)
         also from k have "\<dots> \<le> of_nat k^2" by simp
         finally have "(1 - x^2 / of_nat k^2) \<in> {0..1}" using k
           by (simp_all add: field_simps del: of_nat_Suc)
@@ -3470,7 +3470,7 @@
         by (simp add: eval_nat_numeral)
       from sums_divide[OF this, of "x^3 * pi"] x
         have "(\<lambda>n. - (sin_coeff (n+3) * pi^(n+2) * x^n)) sums ((1 - sin (pi*x) / (pi*x)) / x^2)"
-        by (simp add: field_split_simps eval_nat_numeral power_mult_distrib mult_ac)
+        by (simp add: field_split_simps eval_nat_numeral)
       with x have "(\<lambda>n. - (sin_coeff (n+3) * pi^(n+2) * x^n)) sums (g x / x^2)"
         by (simp add: g_def)
       hence "f' x = g x / x^2" by (simp add: sums_iff f'_def)
@@ -3485,7 +3485,7 @@
         assume x: "x \<noteq> 0"
         from summable_divide[OF sums_summable[OF sums_split_initial_segment[OF
                sin_converges[of "pi*x"]], of 3], of "-pi*x^3"] x
-          show ?thesis by (simp add: mult_ac power_mult_distrib field_split_simps eval_nat_numeral)
+          show ?thesis by (simp add: field_split_simps eval_nat_numeral)
       qed (simp only: summable_0_powser)
     qed
     hence "f' \<midarrow> 0 \<rightarrow> f' 0" by (simp add: isCont_def)
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1526,7 +1526,7 @@
     apply (rule sum.cong)
     using assms
     apply simp
-    apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4))
+    apply (metis abs_of_nonneg content_pos_le)
     done
   have e: "0 \<le> e"
     using assms(2) norm_ge_zero order_trans by blast
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1993,7 +1993,7 @@
       have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
       proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> (*\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> (*\<^sub>R) 2" t])
         show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
-          by (metis \<open>pathstart q' = pathstart q\<close> comp_def h pastq pathstart_def pth_4(2))
+          by (metis \<open>pathstart q' = pathstart q\<close> comp_def h(3) pastq pathstart_def pth_4(2))
         show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
           apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
           using g(2) path_image_def by fastforce+
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Homotopy.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -901,7 +901,7 @@
     apply (rule pip [unfolded path_image_def, THEN subsetD])
     apply (rule image_eqI, blast)
     apply (simp add: algebra_simps)
-    by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono not_le
+    by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono
               add.commute zero_le_numeral)
   have qs: "\<And>a b. \<lbrakk>4 * b \<le> 3; \<not> b * 2 \<le> 1\<rbrakk> \<Longrightarrow> q (4 * b - 2) \<in> s"
     using path_image_def piq by fastforce
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -445,7 +445,7 @@
     obtain u v where K: "K = cbox u v" "K \<noteq> {}" "K \<subseteq> cbox a b"
       using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
     with i show "extend K \<noteq> {}" "extend K \<subseteq> cbox a b"
-      apply (auto simp: extend_def subset_box box_ne_empty sum_if_inner)
+      apply (auto simp: extend_def subset_box box_ne_empty)
       by fastforce
   qed
   have int_extend_disjoint:
@@ -468,7 +468,7 @@
        and xv: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> x \<bullet> k < v \<bullet> k"
        and wx: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> w \<bullet> k < x \<bullet> k"
        and xz: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> x \<bullet> k < z \<bullet> k"
-        using that K1 K2 i by (auto simp: extend_def box_ne_empty sum_if_inner mem_box)
+        using that K1 K2 i by (auto simp: extend_def box_ne_empty mem_box)
       have "box u v \<noteq> {}" "box w z \<noteq> {}"
         using cboxes interior_cbox by (auto simp: content_eq_0_interior dest: mt)
       then obtain q s
@@ -630,7 +630,7 @@
     show "\<Union>Dlec \<subseteq> cbox a b'"
       using Dlec_def div S by (auto simp: b'_def division_of_def mem_box)
     show "(\<forall>K\<in>Dlec. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}) \<or> (\<forall>K\<in>Dlec. K \<inter> {x. x \<bullet> i = b' \<bullet> i} \<noteq> {})"
-      using nonmt by (fastforce simp: Dlec_def b'_def sum_if_inner i)
+      using nonmt by (fastforce simp: Dlec_def b'_def i)
   qed (use i Dlec_def in auto)
   moreover
   have "(\<Sum>K\<in>Dlec. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) =
@@ -640,7 +640,7 @@
     unfolding Dlec_def using \<open>finite \<D>\<close> apply (auto simp: sum.mono_neutral_left)
     done
   moreover have "(b' \<bullet> i - a \<bullet> i) = (c - a \<bullet> i)"
-    by (simp add: b'_def sum_if_inner i)
+    by (simp add: b'_def i)
   ultimately
   have lec: "(c - a \<bullet> i) * (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
              \<le> content(cbox a b')"
@@ -657,7 +657,7 @@
     show "\<Union>Dgec \<subseteq> cbox a' b"
       using Dgec_def div S by (auto simp: a'_def division_of_def mem_box)
     show "(\<forall>K\<in>Dgec. K \<inter> {x. x \<bullet> i = a' \<bullet> i} \<noteq> {}) \<or> (\<forall>K\<in>Dgec. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {})"
-      using nonmt by (fastforce simp: Dgec_def a'_def sum_if_inner i)
+      using nonmt by (fastforce simp: Dgec_def a'_def i)
   qed (use i Dgec_def in auto)
   moreover
   have "(\<Sum>K\<in>Dgec. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) =
@@ -667,7 +667,7 @@
     unfolding Dgec_def using \<open>finite \<D>\<close> apply (auto simp: sum.mono_neutral_left)
     done
   moreover have "(b \<bullet> i - a' \<bullet> i) = (b \<bullet> i - c)"
-    by (simp add: a'_def sum_if_inner i)
+    by (simp add: a'_def i)
   ultimately
   have gec: "(b \<bullet> i - c) * (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
              \<le> content(cbox a' b)"
@@ -679,7 +679,7 @@
     proof
       assume c: "c = a \<bullet> i"
       then have "a' = a"
-        apply (simp add: sum_if_inner i a'_def cong: if_cong)
+        apply (simp add: i a'_def cong: if_cong)
         using euclidean_representation [of a] sum.cong [OF refl, of Basis "\<lambda>i. (a \<bullet> i) *\<^sub>R i"] by presburger
       then have "content (cbox a' b) \<le> 2 * content (cbox a b)"  by simp
       moreover
@@ -701,7 +701,7 @@
     next
       assume c: "c = b \<bullet> i"
       then have "b' = b"
-        apply (simp add: sum_if_inner i b'_def cong: if_cong)
+        apply (simp add: i b'_def cong: if_cong)
         using euclidean_representation [of b] sum.cong [OF refl, of Basis "\<lambda>i. (b \<bullet> i) *\<^sub>R i"] by presburger
       then have "content (cbox a b') \<le> 2 * content (cbox a b)"  by simp
       moreover
@@ -726,14 +726,14 @@
     have prod_if: "(\<Prod>k\<in>Basis \<inter> - {i}. f k) = (\<Prod>k\<in>Basis. f k) / f i" if "f i \<noteq> (0::real)" for f
       using that mk_disjoint_insert [OF i]
       apply (clarsimp simp add: field_split_simps)
-      by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf mult.commute order_refl prod.insert subset_Compl_singleton)
+      by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf order_refl prod.insert subset_Compl_singleton)
     have abc: "a \<bullet> i < c" "c < b \<bullet> i"
       using False assms by auto
     then have "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
                   \<le> content(cbox a b') / (c - a \<bullet> i)"
               "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
                  \<le> content(cbox a' b) / (b \<bullet> i - c)"
-      using lec gec by (simp_all add: field_split_simps mult.commute)
+      using lec gec by (simp_all add: field_split_simps)
     moreover
     have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
           \<le> (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K) +
@@ -780,7 +780,7 @@
           \<le> 2 * content (cbox a b) / (b \<bullet> i - a \<bullet> i)"
       by linarith
     then show ?thesis
-      using abc by (simp add: field_split_simps mult.commute)
+      using abc by (simp add: field_split_simps)
   qed
 qed
 
@@ -856,7 +856,7 @@
   have "gauge (\<lambda>x. ball x
                     (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
     using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b
-    apply (auto simp: gauge_def field_split_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
+    apply (auto simp: gauge_def field_split_simps add_nonneg_eq_0_iff finite_less_Inf_iff)
     apply (meson add_increasing measure_nonneg mult_nonneg_nonneg norm_ge_zero not_le zero_le_numeral)
     done
   then have "gauge \<gamma>"
@@ -936,7 +936,7 @@
               by simp
             also have "... < \<epsilon> * (b \<bullet> i - a \<bullet> i) / dist u v / (4 * content (cbox a b))"
               using duv dist_uv contab_gt0
-              apply (simp add: field_split_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm)
+              apply (simp add: field_split_simps split: if_split_asm)
               by (meson add_nonneg_nonneg linorder_not_le measure_nonneg mult_nonneg_nonneg norm_ge_zero zero_le_numeral)
             also have "... = \<epsilon> * (b \<bullet> i - a \<bullet> i) / norm (v - u) / (4 * content (cbox a b))"
               by (simp add: dist_norm norm_minus_commute)
@@ -1239,7 +1239,7 @@
                 obtain u v where uv: "K = cbox u v"
                   using T''_tagged \<open>(x,K) \<in> T''\<close> by blast
                 then have "connected K"
-                  by (simp add: is_interval_cbox is_interval_connected)
+                  by (simp add: is_interval_connected)
                 then have "(\<exists>z \<in> K. z \<bullet> i = c)"
                   using y connected_ivt_component by fastforce
                 then show ?thesis
@@ -1883,7 +1883,7 @@
   then obtain m::nat where m: "floor(n * f x) = int m"
     using nonneg_int_cases zero_le_floor by blast
   then have kn: "real k / real n \<le> f x \<longleftrightarrow> k \<le> m" for k
-    using \<open>n \<noteq> 0\<close> by (simp add: field_split_simps mult.commute) linarith
+    using \<open>n \<noteq> 0\<close> by (simp add: field_split_simps) linarith
   then have "Suc n / real n \<le> f x \<longleftrightarrow> Suc n \<le> m"
     by blast
   have "real n * f x \<le> real n"
@@ -1894,7 +1894,7 @@
     by (subst sum.inter_restrict) (auto simp: kn)
   also have "\<dots> < inverse n"
     using \<open>m \<le> n\<close> \<open>n \<noteq> 0\<close> m
-    by (simp add: min_absorb2 field_split_simps mult.commute) linarith
+    by (simp add: min_absorb2 field_split_simps) linarith
   finally show ?thesis .
 qed
 
@@ -2222,7 +2222,7 @@
       proof (subst has_integral_cong)
         show "g x * f x - g a * f x = (g b - g a) * h x *\<^sub>R f x"
           if "x \<in> {a..b}" for x
-          using 1 that by (simp add: h_def field_split_simps algebra_simps)
+          using 1 that by (simp add: h_def field_split_simps)
         show "((\<lambda>x. (g b - g a) * h x *\<^sub>R f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
           using has_integral_mult_right [OF c, of "g b - g a"] .
       qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -154,7 +154,7 @@
 lemma abs_summable_on_altdef':
   "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
   unfolding abs_summable_on_def set_integrable_def
-  by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space)
+  by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset sets_count_space space_count_space)
 
 lemma abs_summable_on_norm_iff [simp]:
   "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -624,7 +624,7 @@
         then show "connected (- closure (inside (?\<Theta>1 \<union> ?\<Theta>)))"
           by (metis Compl_Un outside_inside co_out1c closure_Un_frontier)
         have if2: "- (inside (?\<Theta>2 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))) = - ?\<Theta>2 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>2 \<union> ?\<Theta>)"
-          by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c2 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp closure_Un_frontier fr_out(2))
+          by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c2 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp(3) closure_Un_frontier fr_out(2))
         then show "connected (- closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
           by (metis Compl_Un outside_inside co_out2c closure_Un_frontier)
         have "connected(?\<Theta>)"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -684,7 +684,7 @@
       from this elim d[of "rx (ry (rt n))"]
       have "\<dots> < dist (f (?t n) (?y n)) (f (?t n) (?x n)) / rx (ry (rt (n)))"
         using lx'(2) ly'(2) lt'(2) \<open>0 < rx _\<close>
-        by (auto simp add: field_split_simps algebra_simps strict_mono_def)
+        by (auto simp add: field_split_simps strict_mono_def)
       also have "\<dots> \<le> diameter ?S / n"
         by (force intro!: \<open>0 < n\<close> strict_mono_def xy diameter_bounded_bound frac_le
           compact_imp_bounded compact t
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1574,7 +1574,7 @@
   by (cases "emeasure M A" rule: ennreal_cases) (auto simp: measure_def)
 
 lemma measure_zero_top: "emeasure M A = top \<Longrightarrow> measure M A = 0"
-  by (simp add: measure_def enn2ereal_top)
+  by (simp add: measure_def)
 
 lemma measure_eq_emeasure_eq_ennreal: "0 \<le> x \<Longrightarrow> emeasure M A = ennreal x \<Longrightarrow> measure M A = x"
   using emeasure_eq_ennreal_measure[of M A]
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -166,7 +166,7 @@
     (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
     by (auto intro!: sum.cong)
   also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
-    using assms by (auto dest: simple_functionD simp: sum.delta)
+    using assms by (auto dest: simple_functionD)
   also have "... = f x" using x by (auto simp: indicator_def)
   finally show ?thesis by auto
 qed
@@ -327,10 +327,10 @@
     { fix d :: nat
       have "\<lfloor>2^d::real\<rfloor> * \<lfloor>2^m * enn2real (min (of_nat m) (u x))\<rfloor> \<le>
         \<lfloor>2^d * (2^m * enn2real (min (of_nat m) (u x)))\<rfloor>"
-        by (rule le_mult_floor) (auto simp: enn2real_nonneg)
+        by (rule le_mult_floor) (auto)
       also have "\<dots> \<le> \<lfloor>2^d * (2^m * enn2real (min (of_nat d + of_nat m) (u x)))\<rfloor>"
         by (intro floor_mono mult_mono enn2real_mono min.mono)
-           (auto simp: enn2real_nonneg min_less_iff_disj of_nat_less_top)
+           (auto simp: min_less_iff_disj of_nat_less_top)
       finally have "f m x \<le> f (m + d) x"
         unfolding f_def
         by (auto simp: field_simps power_add * simp del: of_int_mult) }
@@ -348,7 +348,7 @@
       by (cases "u x" rule: ennreal_cases)
          (auto split: split_min intro!: floor_mono)
     then have "f i ` space M \<subseteq> (\<lambda>n. real_of_int n / 2^i) ` {0 .. of_nat i * 2^i}"
-      unfolding floor_of_int by (auto simp: f_def enn2real_nonneg intro!: imageI)
+      unfolding floor_of_int by (auto simp: f_def intro!: imageI)
     then show "finite (f i ` space M)"
       by (rule finite_subset) auto
     show "f i \<in> borel_measurable M"
@@ -680,7 +680,7 @@
 proof cases
   assume "finite P"
   from this assms show ?thesis
-    by induct (auto simp: simple_function_sum simple_integral_add sum_nonneg)
+    by induct (auto)
 qed auto
 
 lemma simple_integral_mult[simp]:
@@ -1090,8 +1090,7 @@
   by (subst nn_integral_eq_simple_integral) (auto simp: simple_integral_indicator)
 
 lemma nn_integral_cmult_indicator: "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. c * indicator A x \<partial>M) = c * emeasure M A"
-  by (subst nn_integral_eq_simple_integral)
-     (auto simp: simple_function_indicator simple_integral_indicator)
+  by (subst nn_integral_eq_simple_integral) (auto)
 
 lemma nn_integral_indicator':
   assumes [measurable]: "A \<inter> space M \<in> sets M"
@@ -1120,7 +1119,7 @@
 lemma nn_integral_indicator_singleton'[simp]:
   assumes [measurable]: "{y} \<in> sets M"
   shows "(\<integral>\<^sup>+x. ennreal (f x * indicator {y} x) \<partial>M) = f y * emeasure M {y}"
-  by (subst nn_integral_set_ennreal[symmetric]) (simp add: nn_integral_indicator_singleton)
+  by (subst nn_integral_set_ennreal[symmetric]) (simp)
 
 lemma nn_integral_add:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>N M f + integral\<^sup>N M g"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -48,7 +48,7 @@
 
 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
   and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
-  by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
+  by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib
       cong: if_cong)
 
 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
@@ -118,7 +118,7 @@
   hence "Inf ?proj = x \<bullet> b"
     by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   hence "x \<bullet> b = Inf X \<bullet> b"
-    by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta
+    by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close>
       cong: if_cong)
   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
 qed
@@ -140,7 +140,7 @@
   hence "Sup ?proj = x \<bullet> b"
     by (auto intro!: cSup_eq_maximum)
   hence "x \<bullet> b = Sup X \<bullet> b"
-    by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta
+    by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close>
       cong: if_cong)
   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
 qed
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -511,7 +511,7 @@
    } note ** = this
   show ?thesis
     using assms
-    apply (simp add: arc_def simple_path_def path_join, clarify)
+    apply (simp add: arc_def simple_path_def, clarify)
     apply (simp add: joinpaths_def split: if_split_asm)
     apply (force dest: inj_onD [OF injg1])
     apply (metis *)
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -994,13 +994,13 @@
    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
 unfolding facet_of_def hyperplane_eq_empty
 by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
-           DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
+           Suc_leI of_nat_diff aff_dim_halfspace_le)
 
 lemma hyperplane_facet_of_halfspace_ge:
     "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
 unfolding facet_of_def hyperplane_eq_empty
 by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
-           DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
+           Suc_leI of_nat_diff aff_dim_halfspace_ge)
 
 lemma facet_of_halfspace_le:
     "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
@@ -1316,7 +1316,7 @@
     apply (rule_tac x="u/x" in exI)
     apply (rule_tac x="v/x" in exI)
     apply (rule_tac x="w/x" in exI)
-    using x apply (auto simp: algebra_simps field_split_simps)
+    using x apply (auto simp: field_split_simps)
     done
   ultimately show ?thesis by force
 qed
@@ -1445,14 +1445,14 @@
               have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux"
                 by (metis \<open>ux \<noteq> 0\<close> uxx mult.commute right_inverse scaleR_one scaleR_scaleR)
               also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
-                using \<open>ux \<noteq> 0\<close> equx apply (auto simp: algebra_simps field_split_simps)
+                using \<open>ux \<noteq> 0\<close> equx apply (auto simp: field_split_simps)
                 by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left)
               finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" .
               then have "x \<in> open_segment b c"
                 apply (simp add: in_segment \<open>b \<noteq> c\<close>)
                 apply (rule_tac x="(v * uc) / ux" in exI)
                 using \<open>0 \<le> ux\<close> \<open>ux \<noteq> 0\<close> \<open>0 < uc\<close> \<open>0 < v\<close> \<open>0 < ub\<close> \<open>v < 1\<close> equx
-                apply (force simp: algebra_simps field_split_simps)
+                apply (force simp: field_split_simps)
                 done
               then show ?thesis
                 by (rule face_ofD [OF F _ b c \<open>x \<in> F\<close>])
@@ -2116,7 +2116,7 @@
               done
             then show ?thesis
               using \<open>0 < inff\<close> awlt [OF that] mult_strict_left_mono
-              by (fastforce simp add: algebra_simps field_split_simps split: if_split_asm)
+              by (fastforce simp add: field_split_simps split: if_split_asm)
           next
             case False
             with \<open>0 < inff\<close> have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> 0"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -290,7 +290,7 @@
 next
   case False
   then show ?thesis
-    by (simp add: continuous_compose_quotient_map_eq quotient_map_fst)
+    by (simp add: continuous_compose_quotient_map_eq)
 qed
 
 lemma continuous_map_of_snd:
@@ -302,7 +302,7 @@
 next
   case False
   then show ?thesis
-    by (simp add: continuous_compose_quotient_map_eq quotient_map_snd)
+    by (simp add: continuous_compose_quotient_map_eq)
 qed
 
 lemma continuous_map_prod_top:
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Regularity.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -53,7 +53,7 @@
     hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
     from M_space[OF \<open>1/n>0\<close>]
     have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) \<longlonglongrightarrow> measure M (space M)"
-      unfolding emeasure_eq_measure by (auto simp: measure_nonneg)
+      unfolding emeasure_eq_measure by (auto)
     from metric_LIMSEQ_D[OF this \<open>0 < e * 2 powr -n\<close>]
     obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
       e * 2 powr -n"
@@ -95,7 +95,7 @@
     also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
       by (rule emeasure_subadditive_countably) (auto simp: summable_def)
     also have "\<dots> \<le> (\<Sum>n. ennreal (e*2 powr - real (Suc n)))"
-      using B_compl_le by (intro suminf_le) (simp_all add: measure_nonneg emeasure_eq_measure ennreal_leI)
+      using B_compl_le by (intro suminf_le) (simp_all add: emeasure_eq_measure ennreal_leI)
     also have "\<dots> \<le> (\<Sum>n. ennreal (e * (1 / 2) ^ Suc n))"
       by (simp add: powr_minus powr_realpow field_simps del: of_nat_Suc)
     also have "\<dots> = ennreal e * (\<Sum>n. ennreal ((1 / 2) ^ Suc n))"
@@ -268,7 +268,7 @@
     also have "(\<lambda>n. \<Sum>i<n. M (D i)) \<longlonglongrightarrow> (\<Sum>i. M (D i))"
       by (intro summable_LIMSEQ) auto
     finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) \<longlonglongrightarrow> measure M (\<Union>i. D i)"
-      by (simp add: emeasure_eq_measure measure_nonneg sum_nonneg)
+      by (simp add: emeasure_eq_measure sum_nonneg)
     have "(\<Union>i. D i) \<in> sets M" using \<open>range D \<subseteq> sets M\<close> by auto
 
     case 1
@@ -282,12 +282,12 @@
       then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
         unfolding choice_iff by blast
       have "ennreal (\<Sum>i<n0. measure M (D i)) = (\<Sum>i<n0. M (D i))"
-        by (auto simp add: emeasure_eq_measure sum_nonneg measure_nonneg)
+        by (auto simp add: emeasure_eq_measure)
       also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule sum_le_suminf) auto
       also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
       also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
       finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i<n0. measure M (D i)) < e/2"
-        using n0 by (auto simp: measure_nonneg sum_nonneg)
+        using n0 by (auto simp: sum_nonneg)
       have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
       proof
         fix i
@@ -351,7 +351,7 @@
       have "ennreal (measure M ?U - measure M (\<Union>i. D i)) = M ?U - M (\<Union>i. D i)"
         using U(1,2)
         by (subst ennreal_minus[symmetric])
-           (auto intro!: finite_measure_mono simp: sb measure_nonneg emeasure_eq_measure)
+           (auto intro!: finite_measure_mono simp: sb emeasure_eq_measure)
       also have "\<dots> = M (?U - (\<Union>i. D i))" using U  \<open>(\<Union>i. D i) \<in> sets M\<close>
         by (subst emeasure_Diff) (auto simp: sb)
       also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  \<open>range D \<subseteq> sets M\<close>
@@ -361,7 +361,7 @@
       also have "\<dots> \<le> (\<Sum>i. ennreal e/(2 powr Suc i))" using U \<open>range D \<subseteq> sets M\<close>
         using \<open>0<e\<close>
         by (intro suminf_le, subst emeasure_Diff)
-           (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg ennreal_minus
+           (auto simp: emeasure_Diff emeasure_eq_measure sb ennreal_minus
                        finite_measure_mono divide_ennreal ennreal_less_iff
                  intro: less_imp_le)
       also have "\<dots> \<le> (\<Sum>n. ennreal (e * (1 / 2) ^ Suc n))"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Simplex_Content.thy
--- a/src/HOL/Analysis/Simplex_Content.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Simplex_Content.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -252,7 +252,7 @@
                     ((a + b + c) - 2 * c)"
     unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps)
   also have "\<dots> = 16 * s * (s - a) * (s - b) * (s - c)"
-    by (simp add: s_def field_split_simps mult_ac)
+    by (simp add: s_def field_split_simps)
   finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)"
     by simp
   also have "\<dots> = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -5199,7 +5199,7 @@
         using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
         done
       also have "... = c a + (1 - c a)"
-        by (metis \<open>a \<notin> S\<close> fun_upd_other sum.cong sumSS')
+        by (metis \<open>a \<notin> S\<close> fun_upd_other sum.cong sumSS'(1))
       finally show "sum (cc(a := c a)) (insert a (T \<inter> T')) = 1"
         by simp
       have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = c a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc(a := c a)) x *\<^sub>R x)"
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -149,7 +149,7 @@
   also have "Discrete.log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all
   hence "(\<Sum>k = 2^n..<2^Suc n. f (2^Discrete.log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^n))"
     by (intro sum.cong) simp_all
-  also have "\<dots> = 2^n * f (2^n)" by (simp add: of_nat_power)
+  also have "\<dots> = 2^n * f (2^n)" by (simp)
   finally show ?case by simp
 qed simp
 
@@ -163,7 +163,7 @@
   also have "Discrete.log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all
   hence "(\<Sum>k = 2^n..<2^Suc n. f (2*2^Discrete.log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
     by (intro sum.cong) simp_all
-  also have "\<dots> = 2^n * f (2^Suc n)" by (simp add: of_nat_power)
+  also have "\<dots> = 2^n * f (2^Suc n)" by (simp)
   finally show ?case by simp
 qed simp
 
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -2447,7 +2447,7 @@
               finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
             next
               have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
-                using abi_less by (simp add: field_split_simps algebra_simps)
+                using abi_less by (simp add: field_split_simps)
               also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
                 using aibi [OF \<open>i \<in> Basis\<close>] xab
@@ -2488,12 +2488,12 @@
       proof -
         have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
                   \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
-          by (auto simp: field_split_simps algebra_simps)
+          by (auto simp: field_split_simps)
         have bjaj: "b \<bullet> j - a \<bullet> j > 0"
           using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
         have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
               (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
-          using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps field_split_simps aibi)
+          using that \<open>j \<in> Basis\<close> by (simp add: subset_box field_split_simps aibi)
         then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
           ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
           by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -110,7 +110,7 @@
       then have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
         by (simp add: power2_eq_square)
       then show ?thesis
-        using n by (simp add: sum_divide_distrib field_split_simps mult.commute power2_commute)
+        using n by (simp add: sum_divide_distrib field_split_simps power2_commute)
     qed
     { fix k
       assume k: "k \<le> n"
@@ -158,7 +158,7 @@
     also have "... < e"
       apply (simp add: field_simps)
       using \<open>d>0\<close> nbig e \<open>n>0\<close>
-      apply (simp add: field_split_simps algebra_simps)
+      apply (simp add: field_split_simps)
       using ed0 by linarith
     finally have "\<bar>f x - (\<Sum>k\<le>n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
   }
@@ -576,7 +576,7 @@
   define B where "B j = {x \<in> S. f x \<ge> (j + 1/3)*e}" for j :: nat
   have ngt: "(n-1) * e \<ge> normf f" "n\<ge>1"
     using e
-    apply (simp_all add: n_def field_simps of_nat_Suc)
+    apply (simp_all add: n_def field_simps)
     by (metis real_nat_ceiling_ge mult.commute not_less pos_less_divide_eq)
   then have ge_fx: "(n-1) * e \<ge> f x" if "x \<in> S" for x
     using f normf_upper that by fastforce
@@ -646,7 +646,7 @@
       then have "t \<in> B i"
         using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t
         apply (simp add: A_def B_def)
-        apply (clarsimp simp add: field_simps of_nat_diff not_le of_nat_Suc)
+        apply (clarsimp simp add: field_simps of_nat_diff not_le)
         apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"])
         apply auto
         done
@@ -693,7 +693,7 @@
         apply simp
         apply (rule order_trans [OF _ sum_bounded_below [OF less_imp_le [OF ****]]])
         using True
-        apply (simp_all add: of_nat_Suc of_nat_diff)
+        apply (simp_all add: of_nat_diff)
         done
       also have "... \<le> g t"
         using jn e
@@ -744,7 +744,7 @@
       have "\<not> real (Suc n) < inverse e"
         using \<open>N \<le> n\<close> N using less_imp_inverse_less by force
       then have "1 / (1 + real n) \<le> e"
-        using e by (simp add: field_simps of_nat_Suc)
+        using e by (simp add: field_simps)
       then have "\<bar>f x - g x\<bar> < e"
         using n(2) x by auto
     } note * = this
@@ -927,7 +927,7 @@
   show ?case
     apply (rule_tac x="\<lambda>i. c" in exI)
     apply (rule_tac x=0 in exI)
-    apply (auto simp: mult_ac of_nat_Suc)
+    apply (auto simp: mult_ac)
     done
   case (add f1 f2)
   then obtain a1 n1 a2 n2 where
@@ -1328,7 +1328,7 @@
     also have "... = (\<Sum>j\<in>B. if j = i then x \<bullet> i else 0)"
       by (rule sum.cong; simp)
     also have "... = i \<bullet> x"
-      by (simp add: \<open>finite B\<close> that inner_commute sum.delta)
+      by (simp add: \<open>finite B\<close> that inner_commute)
     finally show ?thesis .
   qed
 qed