# HG changeset patch
# User huffman
# Date 1313945180 25200
# Node ID ea609ebdeebff1dd18ff919c8d7d08b67db45a0b
# Parent  00af710d857e29ca905aec8d8216b282004081d5
section -> subsection

diff -r 00af710d857e -r ea609ebdeebf src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 21 09:38:31 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 21 09:46:20 2011 -0700
@@ -728,7 +728,7 @@
   apply (subst matrix_vector_mul[OF lf])
   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
 
-section {* lambda skolemization on cartesian products *}
+subsection {* lambda skolemization on cartesian products *}
 
 (* FIXME: rename do choice_cart *)
 
@@ -1404,7 +1404,7 @@
   thus ?case using goal1 by auto
 qed
 
-section "Convex Euclidean Space"
+subsection "Convex Euclidean Space"
 
 lemma Cart_1:"(1::real^'n) = (\<chi>\<chi> i. 1)"
   apply(subst euclidean_eq)
diff -r 00af710d857e -r ea609ebdeebf src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 21 09:38:31 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 21 09:46:20 2011 -0700
@@ -3107,7 +3107,7 @@
   shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
   unfolding basis_complex_def by auto
 
-section {* Products Spaces *}
+subsection {* Products Spaces *}
 
 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
   (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)