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 headers
authornipkow
Wed, 16 Jan 2019 10:27:57 +0100
changeset 69665 60110f6d0b4e
parent 69664 839ebe61786f
child 69666 d51e5e41fafe
tuned headers
src/HOL/Analysis/Cartesian_Euclidean_Space.thy file | annotate | diff | comparison | revisions
src/HOL/Analysis/Cartesian_Space.thy file | annotate | diff | comparison | revisions 
--- 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:
--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 05:26:46 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 10:27:57 2019 +0100
@@ -6,6 +6,8 @@
     Author:     Fabian Immler, TUM
 *)
 
+section "Linear Algebra on Finite Cartesian Products"
+
 theory Cartesian_Space
   imports
     Finite_Cartesian_Product Linear_Algebra
isabelle