author nipkow Wed, 16 Jan 2019 15:53:12 +0100 changeset 69667 82bb6225588b parent 69666 d51e5e41fafe child 69668 14a8cac10eac
tuned headers
```--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 11:48:06 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 15:53:12 2019 +0100
@@ -264,7 +264,7 @@
qed

-subsection%important\<open>Some bounds on components etc. relative to operator norm\<close>
+subsection%important\<open>Bounds on components etc.\ relative to operator norm\<close>

lemma%important norm_column_le_onorm:
fixes A :: "real^'n^'m"```
```--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 11:48:06 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 15:53:12 2019 +0100
@@ -13,6 +13,8 @@
Finite_Cartesian_Product Linear_Algebra
begin

+subsection \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close>
+
definition%unimportant "cart_basis = {axis i 1 | i. i\<in>UNIV}"

lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def
@@ -22,7 +24,7 @@
unfolding cart_basis_def Setcompr_eq_image
by (rule card_image) (auto simp: inj_on_def axis_eq_axis)

-interpretation vec: vector_space "(*s) "
+interpretation%important vec: vector_space "(*s) "
by unfold_locales (vector algebra_simps)+

lemma%unimportant independent_cart_basis:
@@ -450,8 +452,8 @@
finally show ?thesis .
qed

-interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a"
-  by unfold_locales (simp_all add: algebra_simps)
+interpretation%important vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a"
+by unfold_locales (simp_all add: algebra_simps)

lemmas [simp del] = vector_space_over_itself.scale_scale
```