diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Power.thy
--- 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])