Even and odd powers of -1

--- a/src/HOL/NatBin.thy	Mon Feb 16 13:38:17 2009 +0100
+++ b/src/HOL/NatBin.thy	Tue Feb 17 10:03:58 2009 +0000
@@ -362,9 +362,14 @@
 unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
 
 lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
-apply (induct "n")
-apply (auto simp add: power_Suc power_add)
-done
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n) then show ?case by (simp add: power_Suc power_add)
+qed
+
+lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
+  by (simp add: power_Suc) 
 
 lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
 by (subst mult_commute) (simp add: power_mult)