--- a/src/HOL/Probability/Sinc_Integral.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy Tue May 24 16:21:49 2022 +0100
@@ -48,7 +48,7 @@
proof (subst interval_integral_FTC_finite)
show "(?F has_vector_derivative exp (- (u * x)) * sin x) (at x within {min 0 t..max 0 t})" for x
by (auto intro!: derivative_eq_intros
- simp: has_field_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
+ simp: has_real_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
(simp_all add: field_simps add_nonneg_eq_0_iff)
qed (auto intro: continuous_at_imp_continuous_on)
@@ -197,7 +197,7 @@
ultimately show ?thesis
using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x]
by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def
- has_field_derivative_iff_has_vector_derivative
+ has_real_derivative_iff_has_vector_derivative
split del: if_split)
qed