src/HOL/Algebra/Exponent.thy
changeset 30240 5b25fee0362c
parent 27717 21bbd410ba04
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -210,12 +210,12 @@
     1.4  
     1.5  lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
     1.6    ==> (p^r) dvd (p^a) - k"
     1.7 -apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
     1.8 +apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
     1.9  apply (subgoal_tac "p^r dvd p^a*m")
    1.10   prefer 2 apply (blast intro: dvd_mult2)
    1.11  apply (drule dvd_diffD1)
    1.12    apply assumption
    1.13 - prefer 2 apply (blast intro: dvd_diff)
    1.14 + prefer 2 apply (blast intro: nat_dvd_diff)
    1.15  apply (drule gr0_implies_Suc, auto)
    1.16  done
    1.17  
    1.18 @@ -226,12 +226,12 @@
    1.19  
    1.20  lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
    1.21    ==> (p^r) dvd (p^a)*m - k"
    1.22 -apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
    1.23 +apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
    1.24  apply (subgoal_tac "p^r dvd p^a*m")
    1.25   prefer 2 apply (blast intro: dvd_mult2)
    1.26  apply (drule dvd_diffD1)
    1.27    apply assumption
    1.28 - prefer 2 apply (blast intro: dvd_diff)
    1.29 + prefer 2 apply (blast intro: nat_dvd_diff)
    1.30  apply (drule less_imp_Suc_add, auto)
    1.31  done
    1.32