src/HOL/Power.thy
changeset 35028 108662d50512
parent 33364 2bd12592c5e8
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Power.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -context ordered_semidom
     1.8 +context linordered_semidom
     1.9  begin
    1.10  
    1.11  lemma zero_less_power [simp]:
    1.12 @@ -323,7 +323,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -context ordered_idom
    1.17 +context linordered_idom
    1.18  begin
    1.19  
    1.20  lemma power_abs: