--- a/src/HOL/Analysis/Derivative.thy Fri Jan 11 11:35:16 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy Fri Jan 11 18:41:50 2019 +0100
@@ -482,7 +482,7 @@
by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
-subsection \<open>Derivatives of local minima and maxima are zero.\<close>
+subsection \<open>Derivatives of local minima and maxima are zero\<close>
lemma has_derivative_local_min:
fixes f :: "'a::real_normed_vector \<Rightarrow> real"