--- a/src/HOL/Real_Vector_Spaces.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Nov 19 10:05:53 2013 +0100
@@ -307,8 +307,8 @@
lemma of_real_numeral: "of_real (numeral w) = numeral w"
using of_real_of_int_eq [of "numeral w"] by simp
-lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w"
-using of_real_of_int_eq [of "neg_numeral w"] by simp
+lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w"
+using of_real_of_int_eq [of "- numeral w"] by simp
text{*Every real algebra has characteristic zero*}
@@ -341,9 +341,6 @@
lemma Reals_numeral [simp]: "numeral w \<in> Reals"
by (subst of_real_numeral [symmetric], rule Reals_of_real)
-lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals"
-by (subst of_real_neg_numeral [symmetric], rule Reals_of_real)
-
lemma Reals_0 [simp]: "0 \<in> Reals"
apply (unfold Reals_def)
apply (rule range_eqI)
@@ -602,7 +599,7 @@
by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
lemma norm_neg_numeral [simp]:
- "norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w"
+ "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
lemma norm_of_int [simp]: