tuned header
authornipkow
Mon Dec 31 12:25:21 2018 +0100 (8 months ago)
changeset 695532c2e2b3e19b7
parent 69552 b85f4c5cb588
child 69554 4d4aedf9e57f
tuned header
src/HOL/Analysis/Derivative.thy
     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)