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