# HG changeset patch
# User nipkow
# Date 1547650392 -3600
# Node ID 82bb6225588ba603cfc698432fb1fc4256cef194
# Parent  d51e5e41fafe5fbd5c60c03980f8dec9d549ec30
tuned headers

diff -r d51e5e41fafe -r 82bb6225588b src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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"
diff -r d51e5e41fafe -r 82bb6225588b src/HOL/Analysis/Cartesian_Space.thy
--- 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