--- 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