| changeset 9969 | 4753185f1dd2 |
| parent 9943 | 55c82decf3f4 |
| child 10142 | d1d61d13e461 |
--- a/src/HOL/NumberTheory/IntPrimes.ML Fri Sep 15 11:34:46 2000 +0200 +++ b/src/HOL/NumberTheory/IntPrimes.ML Fri Sep 15 12:39:57 2000 +0200 @@ -569,7 +569,7 @@ by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); by (subgoal_tac "m*k<m*#1" 1); by (dtac (zmult_zless_cancel1 RS iffD1) 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); qed "zcong_zless_0"; Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";