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)" ? *)