changeset 22957 | 82a799ae7579 |
parent 22955 | 48dc37776d1e |
child 22988 | f6b8184f5b4a |
--- a/src/HOL/Power.thy Sun May 13 20:05:42 2007 +0200 +++ b/src/HOL/Power.thy Mon May 14 08:12:38 2007 +0200 @@ -202,9 +202,7 @@ lemma zero_le_power_abs [simp]: "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" -apply (induct "n") -apply (auto simp add: zero_le_one zero_le_power) -done +by (rule zero_le_power [OF abs_ge_zero]) lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,recpower}) ^ n" proof -