
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
 




