Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
authorpaulson <lp15@cam.ac.uk>
Tue, 22 Sep 2015 16:55:49 +0100
changeset 61235 37862ccec075
parent 61234 a9e6052188fa
child 61236 b033aeaab1b8
SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle