# HG changeset patch
# User immler
# Date 1566915900 -7200
# Node ID 8b7f6ecb33691417e89e08a5abf7e62c73935758
# Parent  7bf683f3672db858aa7702ecf6dc00a74bf68147
moved basic theorem

diff -r 7bf683f3672d -r 8b7f6ecb3369 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Tue Aug 27 13:22:33 2019 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Tue Aug 27 16:25:00 2019 +0200
@@ -8,10 +8,6 @@
   imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
-lemma continuous_on_vector_derivative:
-  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
-  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
-
 definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
 
 lemma einterval_eq[simp]:
diff -r 7bf683f3672d -r 8b7f6ecb3369 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Aug 27 13:22:33 2019 +0200
+++ b/src/HOL/Deriv.thy	Tue Aug 27 16:25:00 2019 +0200
@@ -797,6 +797,10 @@
   "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
 
+lemma continuous_on_vector_derivative:
+  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
+  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+
 lemma has_vector_derivative_mult_right[derivative_intros]:
   fixes a :: "'a::real_normed_algebra"
   shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F"