# HG changeset patch
# User huffman
# Date 1179123158 -7200
# Node ID 82a799ae757945d4d5437979157d81aa3eecd052
# Parent  617140080e6aca23cd5a0f9616e039380190147f
tuned

diff -r 617140080e6a -r 82a799ae7579 src/HOL/Power.thy
--- 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 -