tuned
authorhuffman
Mon May 14 08:12:38 2007 +0200 (2007-05-14)
changeset 2295782a799ae7579
parent 22956 617140080e6a
child 22958 b3a5569a81e5
tuned
src/HOL/Power.thy
     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 -