# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1442937349 -3600
# Node ID 37862ccec075817456845a0f7cf54f8f5d4557cf
# Parent  a9e6052188fae96f304b10e1f766af483e45cadd
SOME rather than THE makes it easy to prove equivalence with other forms of derivatives

diff -r a9e6052188fa -r 37862ccec075 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Sep 22 16:55:07 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Sep 22 16:55:49 2015 +0100
@@ -501,10 +501,10 @@
   unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
 
 definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "deriv f x \<equiv> THE D. DERIV f x :> D"
+  "deriv f x \<equiv> SOME D. DERIV f x :> D"
 
 lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
-  unfolding deriv_def by (metis the_equality DERIV_unique)
+  unfolding deriv_def by (metis some_equality DERIV_unique)
 
 lemma DERIV_deriv_iff_real_differentiable:
   fixes x :: real