# HG changeset patch
# User haftmann
# Date 1240819906 -7200
# Node ID bc4117fe72ab3afd77161af6a32636d89aecca26
# Parent  7e6ffd8f51a92a595451f3f3f1ce6d08bb62b8c6
whitespace tuning

diff -r 7e6ffd8f51a9 -r bc4117fe72ab src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Mon Apr 27 10:11:44 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy	Mon Apr 27 10:11:46 2009 +0200
@@ -396,10 +396,10 @@
   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)
+  by (subst mult_commute) (simp add: power_mult)
 
 lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
-by (simp add: power_even_eq) 
+  by (simp add: power_even_eq)
 
 lemma power_minus_even [simp]:
   "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"