# HG changeset patch # User haftmann # Date 1273180318 -7200 # Node ID c8ea75ea4a29db002fc64acc8249c45734a2a27b # Parent bfd7f5c3bf692d3605e9f04dc618fef5617b1d86 tuned proof diff -r bfd7f5c3bf69 -r c8ea75ea4a29 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu May 06 23:11:57 2010 +0200 +++ b/src/HOL/Parity.thy Thu May 06 23:11:58 2010 +0200 @@ -229,7 +229,7 @@ lemma zero_le_odd_power: "odd n ==> (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff) -apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) +apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square) done lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =