Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 69665 60110f6d0b4e
parent 69663 41ff40bf1530
child 69666 d51e5e41fafe 
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 05:26:46 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 10:27:57 2019 +0100
@@ -801,7 +801,7 @@
 qed
 
 
-subsection%important \<open>Component of the differential must be zero if it exists at a local
+text%important \<open>Component of the differential must be zero if it exists at a local
   maximum or minimum for that corresponding component\<close>
 
 lemma%important differential_zero_maxmin_cart:
isabelle