# 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) =