--- a/src/HOL/NumberTheory/Chinese.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Fri Sep 10 20:04:14 2004 +0200
@@ -92,10 +92,9 @@
"k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
apply (induct l)
apply auto
- apply (rule_tac [2] zdvd_zmult2)
- apply (rule_tac [3] zdvd_zmult)
- apply (subgoal_tac "i = k")
- apply (subgoal_tac [3] "i = Suc (k + n)")
+ apply (rule_tac [1] zdvd_zmult2)
+ apply (rule_tac [2] zdvd_zmult)
+ apply (subgoal_tac "i = Suc (k + n)")
apply (simp_all (no_asm_simp))
done