src/HOL/Analysis/Derivative.thy
changeset 69553 2c2e2b3e19b7
parent 69529 4ab9657b3257
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Analysis/Derivative.thy	Sun Dec 30 17:44:33 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Derivative.thy	Mon Dec 31 12:25:21 2018 +0100
     1.3 @@ -2193,7 +2193,7 @@
     1.4    using assms(2-3) vector_derivative_works
     1.5    by auto
     1.6  
     1.7 -subsection\<open>The notion of being field differentiable\<close>
     1.8 +subsection \<open>Field differentiability\<close>
     1.9  
    1.10  definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
    1.11             (infixr "(field'_differentiable)" 50)