1.1 --- a/src/HOL/Nat_Numeral.thy	Mon Apr 27 10:11:44 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Mon Apr 27 10:11:46 2009 +0200
     1.3 @@ -396,10 +396,10 @@
     1.4    by (simp add: power_Suc) 
     1.5  
     1.6  lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
     1.7 -by (subst mult_commute) (simp add: power_mult)
     1.8 +  by (subst mult_commute) (simp add: power_mult)
     1.9  
    1.10  lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
    1.11 -by (simp add: power_even_eq) 
    1.12 +  by (simp add: power_even_eq)
    1.13  
    1.14  lemma power_minus_even [simp]:
    1.15    "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"