src/HOL/Analysis/Product_Vector.thy

--- a/src/HOL/Analysis/Product_Vector.thy	Fri Apr 12 22:09:25 2019 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy	Fri Apr 12 22:24:07 2019 +0200
@@ -354,6 +354,7 @@
 
 subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Frechet derivatives involving pairs\<close>
 
+text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
 proposition has_derivative_Pair [derivative_intros]:
   assumes f: "(f has_derivative f') (at x within s)"
     and g: "(g has_derivative g') (at x within s)"