| changeset 10658 | b9d43a2add79 |
| parent 10175 | 76646fc8b1bf |
| child 10961 | 74817560a8e8 |
--- a/src/HOL/NumberTheory/Chinese.ML Wed Dec 13 10:31:08 2000 +0100 +++ b/src/HOL/NumberTheory/Chinese.ML Wed Dec 13 10:31:46 2000 +0100 @@ -99,7 +99,7 @@ by (res_inst_tac [("k","kf n")] zcong_cancel2 1); by (res_inst_tac [("b","bf n")] zcong_trans 3); by (stac zcong_sym 4); -by (rtac zless_imp_zle 1); +by (rtac order_less_imp_le 1); by (ALLGOALS Asm_simp_tac); val lemma = result();