Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned spacing;
authorwenzelm
Fri, 12 Apr 2019 22:24:07 +0200
changeset 70137 824c047db30b
parent 70136 f03a01a18c6e
child 70138 bd42cc1e10d0
tuned spacing;
src/HOL/Analysis/Product_Vector.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle