author huffman Sun Aug 21 09:46:20 2011 -0700 (2011-08-21) changeset 44360 ea609ebdeebf parent 44359 00af710d857e child 44361 75ec83d45303
section -> subsection
```     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.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)" ? *)
```