src/HOL/Real_Vector_Spaces.thy
changeset 54489 03ff4d1e6784
parent 54263 c4159fe6fa46
child 54703 499f92dc6e45
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -307,8 +307,8 @@
     1.4  lemma of_real_numeral: "of_real (numeral w) = numeral w"
     1.5  using of_real_of_int_eq [of "numeral w"] by simp
     1.6  
     1.7 -lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w"
     1.8 -using of_real_of_int_eq [of "neg_numeral w"] by simp
     1.9 +lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w"
    1.10 +using of_real_of_int_eq [of "- numeral w"] by simp
    1.11  
    1.12  text{*Every real algebra has characteristic zero*}
    1.13  
    1.14 @@ -341,9 +341,6 @@
    1.15  lemma Reals_numeral [simp]: "numeral w \<in> Reals"
    1.16  by (subst of_real_numeral [symmetric], rule Reals_of_real)
    1.17  
    1.18 -lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals"
    1.19 -by (subst of_real_neg_numeral [symmetric], rule Reals_of_real)
    1.20 -
    1.21  lemma Reals_0 [simp]: "0 \<in> Reals"
    1.22  apply (unfold Reals_def)
    1.23  apply (rule range_eqI)
    1.24 @@ -602,7 +599,7 @@
    1.25  by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
    1.26  
    1.27  lemma norm_neg_numeral [simp]:
    1.28 -  "norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w"
    1.29 +  "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
    1.30  by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
    1.31  
    1.32  lemma norm_of_int [simp]: