Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Characteristic_Functions.thy
changeset 75462 7448423e5dba
parent 70365 4df0628e8545
child 79599 2c18ac57e92e 
--- a/src/HOL/Probability/Characteristic_Functions.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Tue May 24 16:21:49 2022 +0100
@@ -238,7 +238,7 @@
     have "LBINT s=0..x. (x - s)^n = ?F x - ?F 0"
       unfolding zero_ereal_def
       by (intro interval_integral_FTC_finite continuous_at_imp_continuous_on
-                has_field_derivative_iff_has_vector_derivative[THEN iffD1])
+                has_real_derivative_iff_has_vector_derivative[THEN iffD1])
          (auto simp del: power_Suc intro!: derivative_eq_intros simp add: add_nonneg_eq_0_iff)
     also have "\<dots> = x ^ (Suc n) / (Suc n)" by simp
     finally show ?thesis .
isabelle