1.1 --- a/src/HOL/Power.thy	Tue Jul 12 12:49:46 2005 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Jul 12 17:56:03 2005 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  lemma zero_less_power:
     1.5       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
     1.6  apply (induct "n")
     1.7 -apply (simp_all add: power_Suc zero_less_one mult_pos)
     1.8 +apply (simp_all add: power_Suc zero_less_one mult_pos_pos)
     1.9  done
    1.10  
    1.11  lemma zero_le_power:
    1.12 @@ -165,6 +165,12 @@
    1.13  apply (auto simp add: power_Suc inverse_mult_distrib)
    1.14  done
    1.15  
    1.16 +lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = 
    1.17 +    (1 / a)^n"
    1.18 +apply (simp add: divide_inverse)
    1.19 +apply (rule power_inverse)
    1.20 +done
    1.21 +
    1.22  lemma nonzero_power_divide:
    1.23      "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)"
    1.24  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)