# HG changeset patch
# User wenzelm
# Date 1555100647 -7200
# Node ID 824c047db30bdaf136e33df6a57a05d40ca51642
# Parent  f03a01a18c6ee3d4cfa815adb8421d4a1c30099a
tuned spacing;

diff -r f03a01a18c6e -r 824c047db30b 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)"