changeset 35043 | 07dbdf60d5ad |
parent 35028 | 108662d50512 |
child 35216 | 7641e8d831d2 |
--- a/src/HOL/Parity.thy Mon Feb 08 14:22:22 2010 +0100 +++ b/src/HOL/Parity.thy Mon Feb 08 14:22:22 2010 +0100 @@ -218,7 +218,7 @@ done lemma zero_le_even_power: "even n ==> - 0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n" + 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n" apply (simp add: even_nat_equiv_def2) apply (erule exE) apply (erule ssubst)