changeset 13630 | a013a9dd370f |
parent 13601 | fd3e3d6b37b2 |
child 13788 | fd03c4ab89d4 |
--- a/src/HOL/NumberTheory/IntPrimes.thy Mon Oct 07 19:01:51 2002 +0200 +++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Oct 08 08:20:17 2002 +0200 @@ -582,7 +582,6 @@ apply (unfold zcong_def dvd_def) apply auto apply (subgoal_tac "0 < m") - apply (rotate_tac -1) apply (simp add: int_0_le_mult_iff) apply (subgoal_tac "m * k < m * 1") apply (drule zmult_zless_cancel1 [THEN iffD1])