src/HOL/Algebra/Exponent.thy
changeset 16733 236dfafbeb63
parent 16663 13e9c402308b
child 20282 49c312eaaa11
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Thu Jul 07 12:36:56 2005 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Jul 07 12:39:17 2005 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  apply (case_tac "k=0", simp)
     1.5  apply (drule_tac x = m in spec)
     1.6  apply (drule_tac x = k in spec)
     1.7 -apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
     1.8 +apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2)
     1.9  done
    1.10  
    1.11  lemma zero_less_prime_power: "prime p ==> 0 < p^a"