| changeset 10175 | 76646fc8b1bf |
| parent 9943 | 55c82decf3f4 |
| child 10658 | b9d43a2add79 |
--- a/src/HOL/NumberTheory/Chinese.ML Mon Oct 09 12:25:10 2000 +0200 +++ b/src/HOL/NumberTheory/Chinese.ML Mon Oct 09 14:10:55 2000 +0200 @@ -210,7 +210,7 @@ by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7); by (rewtac xilin_sol_def); by (Asm_simp_tac 7); -by (rtac (ex1_implies_ex RS ex_someI) 7); +by (rtac (ex1_implies_ex RS someI_ex) 7); by (rtac unique_xi_sol 7); by (rtac funprod_zdvd 4); by (rewtac m_cond_def);