# HG changeset patch
# User nipkow
# Date 1546255521 -3600
# Node ID 2c2e2b3e19b7dcf9d71d7cc69a2baaeeb7322b4e
# Parent  b85f4c5cb58882ed6c47933138376e6182a3ff29
tuned header

diff -r b85f4c5cb588 -r 2c2e2b3e19b7 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)