# HG changeset patch
# User huffman
# Date 1333024975 -7200
# Node ID 836bf25fb70f61c84c000bc17961b654556e673c
# Parent  6e53f2a718c21358b3053e68a8aeeb9a427e0cf6
remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}

diff -r 6e53f2a718c2 -r 836bf25fb70f src/HOL/NSA/HyperDef.thy
--- 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"
diff -r 6e53f2a718c2 -r 836bf25fb70f src/HOL/Nat_Numeral.thy
--- 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}*}