--- a/src/HOL/Power.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Power.thy Mon Nov 02 11:56:28 2015 +0100
@@ -283,6 +283,9 @@
by (simp del: power_Suc add: power_Suc2 mult.assoc)
qed
+lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
+ by (rule power_minus)
+
lemma power_minus_Bit0:
"(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
by (induct k, simp_all only: numeral_class.numeral.simps power_add
@@ -307,7 +310,7 @@
lemma power_minus1_odd:
"(- 1) ^ Suc (2*n) = -1"
by simp
-
+
lemma power_minus_even [simp]:
"(-a) ^ (2*n) = a ^ (2*n)"
by (simp add: power_minus [of a])