--- 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