diff -r f424e164d752 -r 5e315defb038 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Deriv.thy	Mon May 11 11:15:41 2020 +0100
@@ -572,6 +572,7 @@
     bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
   using has_derivative_within [of f f' x UNIV]
   by simp
+
 lemma has_derivative_zero_unique:
   assumes "((\<lambda>x. 0) has_derivative F) (at x)"
   shows "F = (\<lambda>h. 0)"
@@ -618,6 +619,9 @@
     unfolding fun_eq_iff right_minus_eq .
 qed
 
+lemma has_derivative_Uniq: "\<exists>\<^sub>\<le>\<^sub>1F. (f has_derivative F) (at x)"
+  by (simp add: Uniq_def has_derivative_unique)
+
 
 subsection \<open>Differentiability predicate\<close>
 
@@ -970,6 +974,9 @@
 lemma DERIV_unique: "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
   unfolding DERIV_def by (rule LIM_unique)
 
+lemma DERIV_Uniq: "\<exists>\<^sub>\<le>\<^sub>1D. DERIV f x :> D"
+  by (simp add: DERIV_unique Uniq_def)
+
 lemma DERIV_sum[derivative_intros]:
   "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow>
     ((\<lambda>x. sum (f x) S) has_field_derivative sum (f' x) S) F"