src/HOL/Power.thy
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: