src/HOL/Analysis/Derivative.thy

--- 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)