src/HOL/Parity.thy
changeset 35043 07dbdf60d5ad
parent 35028 108662d50512
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Parity.thy	Mon Feb 08 14:22:22 2010 +0100
     1.2 +++ b/src/HOL/Parity.thy	Mon Feb 08 14:22:22 2010 +0100
     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::{linlinordered_ring_strict,monoid_mult}) ^ n"
     1.8 +    0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
     1.9    apply (simp add: even_nat_equiv_def2)
    1.10    apply (erule exE)
    1.11    apply (erule ssubst)