--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 23:43:22 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 17:32:02 2011 -0700
@@ -126,7 +126,7 @@
lemmas isCont_euclidean_component [simp] =
bounded_linear.isCont [OF bounded_linear_euclidean_component]
-lemma euclidean_component_zero: "0 $$ i = 0"
+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"