changeset 23315 | df3a7e9ebadb |
parent 21404 | eb85850d3eb7 |
child 23894 | 1a4167d761ac |
--- a/src/HOL/NumberTheory/Chinese.thy Mon Jun 11 11:06:00 2007 +0200 +++ b/src/HOL/NumberTheory/Chinese.thy Mon Jun 11 11:06:04 2007 +0200 @@ -197,7 +197,14 @@ apply (rule_tac [3] zdvd_zmult2) apply (rule_tac [4] zdvd_zmult) apply (rule_tac [!] funprod_zdvd) - apply arith+ + apply arith + apply arith + apply arith + apply arith + apply arith + apply arith + apply arith + apply arith done lemma x_sol_lin: