# HG changeset patch
# User nipkow
# Date 1547630877 -3600
# Node ID 60110f6d0b4e239e9c403e9ea93182cd820d282e
# Parent  839ebe61786f0e8e77e15621720d280f88f5f132
tuned headers

diff -r 839ebe61786f -r 60110f6d0b4e src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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:
diff -r 839ebe61786f -r 60110f6d0b4e src/HOL/Analysis/Cartesian_Space.thy
--- 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