src/HOL/Power.thy
changeset 25231 1aa9c8f022d0
parent 25162 ad4d5365d9d8
child 25836 f7771e4f7064
     1.1 --- a/src/HOL/Power.thy	Tue Oct 30 08:45:54 2007 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Oct 30 08:45:55 2007 +0100
     1.3 @@ -194,7 +194,8 @@
     1.4      show ?case by (simp add: zero_less_one)
     1.5  next
     1.6    case (Suc n)
     1.7 -    show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
     1.8 +    show ?case by (auto simp add: prems power_Suc zero_less_mult_iff
     1.9 +      abs_zero)
    1.10  qed
    1.11  
    1.12  lemma zero_le_power_abs [simp]: