src/HOL/NumberTheory/Chinese.thy
changeset 15197 19e735596e51
parent 14353 79f9fbef9106
child 15236 f289e8ba2bb3
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Fri Sep 10 14:54:54 2004 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Fri Sep 10 20:04:14 2004 +0200
     1.3 @@ -92,10 +92,9 @@
     1.4      "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
     1.5    apply (induct l)
     1.6     apply auto
     1.7 -    apply (rule_tac [2] zdvd_zmult2)
     1.8 -    apply (rule_tac [3] zdvd_zmult)
     1.9 -    apply (subgoal_tac "i = k")
    1.10 -    apply (subgoal_tac [3] "i = Suc (k + n)")
    1.11 +    apply (rule_tac [1] zdvd_zmult2)
    1.12 +    apply (rule_tac [2] zdvd_zmult)
    1.13 +    apply (subgoal_tac "i = Suc (k + n)")
    1.14      apply (simp_all (no_asm_simp))
    1.15    done
    1.16