diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -207,6 +207,15 @@
     by (auto intro!: injI simp add: vec_eq_iff of_nat_index)
 qed
 
+instance vec :: (numeral, finite) numeral ..
+instance vec :: (semiring_numeral, finite) semiring_numeral ..
+
+lemma numeral_index [simp]: "numeral w $ i = numeral w"
+  by (induct w, simp_all only: numeral.simps vector_add_component one_index)
+
+lemma neg_numeral_index [simp]: "neg_numeral w $ i = neg_numeral w"
+  by (simp only: neg_numeral_def vector_uminus_component numeral_index)
+
 instance vec :: (comm_ring_1, finite) comm_ring_1 ..
 instance vec :: (ring_char_0, finite) ring_char_0 ..
 
@@ -222,7 +231,7 @@
   by (vector field_simps)
 lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
 lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
-lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector
+lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector
 lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
 lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
   by (vector field_simps)