diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/Power.thy
--- 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: