src/HOL/Algebra/Exponent.thy
changeset 27651 16a26996c30e
parent 27105 5f139027c365
child 27717 21bbd410ba04
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Jul 18 17:09:48 2008 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Jul 18 18:25:53 2008 +0200
     1.3 @@ -49,8 +49,7 @@
     1.4  apply (erule disjE)
     1.5  apply (rule disjI1)
     1.6  apply (rule_tac [2] disjI2)
     1.7 -apply (erule_tac n = m in dvdE)
     1.8 -apply (erule_tac [2] n = n in dvdE, auto)
     1.9 +apply (auto elim!: dvdE)
    1.10  done
    1.11  
    1.12  
    1.13 @@ -202,7 +201,7 @@
    1.14  apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
    1.15  apply (drule less_imp_le [of a])
    1.16  apply (drule le_imp_power_dvd)
    1.17 -apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
    1.18 +apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
    1.19  apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
    1.20  done
    1.21