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.
tuned header
authornipkow
Mon, 31 Dec 2018 12:25:21 +0100
changeset 69553 2c2e2b3e19b7
parent 69552 b85f4c5cb588
child 69554 4d4aedf9e57f
tuned header
src/HOL/Analysis/Derivative.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Analysis/Derivative.thy	Sun Dec 30 17:44:33 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Mon Dec 31 12:25:21 2018 +0100
@@ -2193,7 +2193,7 @@
   using assms(2-3) vector_derivative_works
   by auto
 
-subsection\<open>The notion of being field differentiable\<close>
+subsection \<open>Field differentiability\<close>
 
 definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
            (infixr "(field'_differentiable)" 50)
isabelle