1.1 --- a/src/HOL/Divides.thy	Mon Apr 27 19:44:30 2009 -0700
     1.2 +++ b/src/HOL/Divides.thy	Tue Apr 28 13:34:45 2009 +0200
     1.3 @@ -333,8 +333,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
     1.8 -    (x div y)^n = x^n div y^n"
     1.9 +lemma div_power:
    1.10 +  "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
    1.11 +    (x div y) ^ n = x ^ n div y ^ n"
    1.12  apply (induct n)
    1.13   apply simp
    1.14  apply(simp add: div_mult_div_if_dvd dvd_power_same)
    1.15 @@ -936,10 +937,8 @@
    1.16  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
    1.17    by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
    1.18  
    1.19 -lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    1.20 -  by (induct n) auto
    1.21 -
    1.22 -lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
    1.23 +lemma power_dvd_imp_le:
    1.24 +  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
    1.25    apply (rule power_le_imp_le_exp, assumption)
    1.26    apply (erule dvd_imp_le, simp)
    1.27    done