changeset 35028 | 108662d50512 |
parent 33364 | 2bd12592c5e8 |
child 35216 | 7641e8d831d2 |
--- a/src/HOL/Power.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/Power.thy Fri Feb 05 14:33:50 2010 +0100 @@ -130,7 +130,7 @@ end -context ordered_semidom +context linordered_semidom begin lemma zero_less_power [simp]: @@ -323,7 +323,7 @@ end -context ordered_idom +context linordered_idom begin lemma power_abs: