# 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}) \ (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 -