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