diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/NatBin.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -376,13 +376,13 @@
      "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
 proof (induct "n")
   case 0
-    show ?case by (simp add: Power.power_Suc)
+  then show ?case by (simp add: Power.power_Suc)
 next
   case (Suc n)
-    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
-      by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
-    thus ?case
-      by (simp add: prems mult_less_0_iff mult_neg_neg)
+  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
+    by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
+  thus ?case
+    by (simp add: prems mult_less_0_iff mult_neg_neg)
 qed
 
 lemma odd_0_le_power_imp_0_le: