consider changes variable names in theorem le_imp_power_dvd
authorhaftmann
Fri Feb 20 14:49:23 2009 +0100 (2009-02-20)
changeset 30011cc264a9a033d
parent 30010 862fc7751a15
child 30012 a717c3dffe4f
consider changes variable names in theorem le_imp_power_dvd
src/HOL/Algebra/Exponent.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Feb 20 10:14:32 2009 +0100
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Feb 20 14:49:23 2009 +0100
     1.3 @@ -210,7 +210,7 @@
     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 @@ -226,7 +226,7 @@
    1.13  
    1.14  lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
    1.15    ==> (p^r) dvd (p^a)*m - k"
    1.16 -apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
    1.17 +apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
    1.18  apply (subgoal_tac "p^r dvd p^a*m")
    1.19   prefer 2 apply (blast intro: dvd_mult2)
    1.20  apply (drule dvd_diffD1)