1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
     1.3 @@ -126,7 +126,7 @@
     1.4  lemmas isCont_euclidean_component [simp] =
     1.5    bounded_linear.isCont [OF bounded_linear_euclidean_component]
     1.6  
     1.7 -lemma euclidean_component_zero: "0 $$ i = 0"
     1.8 +lemma euclidean_component_zero [simp]: "0 $$ i = 0"
     1.9    unfolding euclidean_component_def by (rule inner_zero_right)
    1.10  
    1.11  lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"