--- 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: