diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -129,19 +129,19 @@
 lemma euclidean_component_zero [simp]: "0 $$ i = 0"
   unfolding euclidean_component_def by (rule inner_zero_right)
 
-lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
+lemma euclidean_component_add [simp]: "(x + y) $$ i = x $$ i + y $$ i"
   unfolding euclidean_component_def by (rule inner_add_right)
 
-lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
+lemma euclidean_component_diff [simp]: "(x - y) $$ i = x $$ i - y $$ i"
   unfolding euclidean_component_def by (rule inner_diff_right)
 
-lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
+lemma euclidean_component_minus [simp]: "(- x) $$ i = - (x $$ i)"
   unfolding euclidean_component_def by (rule inner_minus_right)
 
-lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
+lemma euclidean_component_scaleR [simp]: "(scaleR a x) $$ i = a * (x $$ i)"
   unfolding euclidean_component_def by (rule inner_scaleR_right)
 
-lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
+lemma euclidean_component_setsum [simp]: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
   unfolding euclidean_component_def by (rule inner_setsum_right)
 
 lemma euclidean_eqI:
@@ -183,7 +183,6 @@
   fixes x :: "'a::euclidean_space"
   shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
   apply (rule euclidean_eqI)
-  apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
   apply (simp add: if_distrib setsum_delta cong: if_cong)
   done
 
@@ -194,8 +193,7 @@
 
 lemma euclidean_lambda_beta [simp]:
   "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
-  by (auto simp: euclidean_component_setsum euclidean_component_scaleR
-    Chi_def if_distrib setsum_cases intro!: setsum_cong)
+  by (auto simp: Chi_def if_distrib setsum_cases intro!: setsum_cong)
 
 lemma euclidean_lambda_beta':
   "j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"