src/HOL/Algebra/Exponent.thy
changeset 31952 40501bb2d57c
parent 31717 d1f7b6245a75
child 32480 6c19da8e661a
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Jul 07 07:56:24 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Jul 07 17:39:51 2009 +0200
     1.3 @@ -217,7 +217,7 @@
     1.4   prefer 2 apply (blast intro: dvd_mult2)
     1.5  apply (drule dvd_diffD1)
     1.6    apply assumption
     1.7 - prefer 2 apply (blast intro: nat_dvd_diff)
     1.8 + prefer 2 apply (blast intro: dvd_diff_nat)
     1.9  apply (drule gr0_implies_Suc, auto)
    1.10  done
    1.11  
    1.12 @@ -233,7 +233,7 @@
    1.13   prefer 2 apply (blast intro: dvd_mult2)
    1.14  apply (drule dvd_diffD1)
    1.15    apply assumption
    1.16 - prefer 2 apply (blast intro: nat_dvd_diff)
    1.17 + prefer 2 apply (blast intro: dvd_diff_nat)
    1.18  apply (drule less_imp_Suc_add, auto)
    1.19  done
    1.20