src/HOL/Algebra/Exponent.thy
changeset 23976 9a1859635978
parent 21256 47195501ecf7
child 24742 73b8b42a36b6
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Jul 24 22:59:53 2007 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Jul 24 23:55:28 2007 +0200
     1.3 @@ -51,9 +51,6 @@
     1.4  apply (rule_tac [2] disjI2)
     1.5  apply (erule_tac n = m in dvdE)
     1.6  apply (erule_tac [2] n = n in dvdE, auto)
     1.7 -apply (rule_tac [2] k = p in dvd_mult_cancel)
     1.8 -apply (rule_tac k = p in dvd_mult_cancel)
     1.9 -apply (simp_all add: mult_ac)
    1.10  done
    1.11  
    1.12  
    1.13 @@ -77,7 +74,6 @@
    1.14   apply (drule_tac x = nat in spec)
    1.15   apply (drule_tac x = b in spec)
    1.16   apply simp
    1.17 - apply (blast intro: dvd_refl mult_dvd_mono)
    1.18  (*case 2: p dvd n*)
    1.19  apply (case_tac "b")
    1.20   apply simp
    1.21 @@ -85,7 +81,6 @@
    1.22  apply (drule spec, drule spec, erule (1) notE impE)
    1.23  apply (drule_tac x = a in spec)
    1.24  apply (drule_tac x = nat in spec, simp)
    1.25 -apply (blast intro: dvd_refl mult_dvd_mono)
    1.26  done
    1.27  
    1.28  (*needed in this form in Sylow.ML*)