src/HOL/Parity.thy
changeset 36722 c8ea75ea4a29
parent 35644 d20cf282342e
child 36840 1e020f445846
     1.1 --- a/src/HOL/Parity.thy	Thu May 06 23:11:57 2010 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu May 06 23:11:58 2010 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4  lemma zero_le_odd_power: "odd n ==>
     1.5      (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
     1.6  apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
     1.7 -apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
     1.8 +apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
     1.9  done
    1.10  
    1.11  lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =