remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}

--- a/src/HOL/NSA/HyperDef.thy	Thu Mar 29 14:39:05 2012 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Thu Mar 29 14:42:55 2012 +0200
@@ -538,7 +538,7 @@
 
 lemma hyperpow_minus_one2 [simp]:
      "\<And>n. -1 pow (2*n) = (1::hypreal)"
-by transfer (rule power_m1_even)
+by transfer (rule power_minus1_even)
 
 lemma hyperpow_less_le:
      "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"

--- a/src/HOL/Nat_Numeral.thy	Thu Mar 29 14:39:05 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Thu Mar 29 14:42:55 2012 +0200
@@ -200,12 +200,6 @@
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (fact Let_def)
 
-lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::ring_1)"
-  by (fact power_minus1_even) (* FIXME: duplicate *)
-
-lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::ring_1)"
-  by (fact power_minus1_odd) (* FIXME: duplicate *)
-
 
 subsection{*Literal arithmetic and @{term of_nat}*}