src/HOL/Parity.thy
changeset 35631 0b8a5fd339ab
parent 35216 7641e8d831d2
child 35644 d20cf282342e
     1.1 --- a/src/HOL/Parity.thy	Sat Mar 06 16:02:22 2010 -0800
     1.2 +++ b/src/HOL/Parity.thy	Sat Mar 06 18:24:30 2010 -0800
     1.3 @@ -218,7 +218,7 @@
     1.4    done
     1.5  
     1.6  lemma zero_le_even_power: "even n ==>
     1.7 -    0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
     1.8 +    0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
     1.9    apply (simp add: even_nat_equiv_def2)
    1.10    apply (erule exE)
    1.11    apply (erule ssubst)