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