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