section -> subsection
authorhuffman
Sun Aug 21 09:46:20 2011 -0700 (2011-08-21)
changeset 44360ea609ebdeebf
parent 44359 00af710d857e
child 44361 75ec83d45303
section -> subsection
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 21 09:38:31 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 21 09:46:20 2011 -0700
     1.3 @@ -728,7 +728,7 @@
     1.4    apply (subst matrix_vector_mul[OF lf])
     1.5    unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
     1.6  
     1.7 -section {* lambda skolemization on cartesian products *}
     1.8 +subsection {* lambda skolemization on cartesian products *}
     1.9  
    1.10  (* FIXME: rename do choice_cart *)
    1.11  
    1.12 @@ -1404,7 +1404,7 @@
    1.13    thus ?case using goal1 by auto
    1.14  qed
    1.15  
    1.16 -section "Convex Euclidean Space"
    1.17 +subsection "Convex Euclidean Space"
    1.18  
    1.19  lemma Cart_1:"(1::real^'n) = (\<chi>\<chi> i. 1)"
    1.20    apply(subst euclidean_eq)
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 21 09:38:31 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 21 09:46:20 2011 -0700
     2.3 @@ -3107,7 +3107,7 @@
     2.4    shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
     2.5    unfolding basis_complex_def by auto
     2.6  
     2.7 -section {* Products Spaces *}
     2.8 +subsection {* Products Spaces *}
     2.9  
    2.10  lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
    2.11    (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)