src/HOL/NumberTheory/Chinese.thy
changeset 15236 f289e8ba2bb3
parent 15197 19e735596e51
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Oct 11 07:39:19 2004 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Mon Oct 11 07:42:22 2004 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4     apply auto
     1.5      apply (rule_tac [1] zdvd_zmult2)
     1.6      apply (rule_tac [2] zdvd_zmult)
     1.7 -    apply (subgoal_tac "i = Suc (k + n)")
     1.8 +    apply (subgoal_tac "i = Suc (k + l)")
     1.9      apply (simp_all (no_asm_simp))
    1.10    done
    1.11  
    1.12 @@ -125,11 +125,11 @@
    1.13     apply clarify
    1.14     apply (subgoal_tac "k = j")
    1.15      apply (simp_all (no_asm_simp))
    1.16 -  apply (case_tac "Suc (k + n) = j")
    1.17 -   apply (subgoal_tac "funsum f k n = 0")
    1.18 +  apply (case_tac "Suc (k + l) = j")
    1.19 +   apply (subgoal_tac "funsum f k l = 0")
    1.20      apply (rule_tac [2] funsum_zero)
    1.21 -    apply (subgoal_tac [3] "f (Suc (k + n)) = 0")
    1.22 -     apply (subgoal_tac [3] "j \<le> k + n")
    1.23 +    apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
    1.24 +     apply (subgoal_tac [3] "j \<le> k + l")
    1.25        prefer 4
    1.26        apply arith
    1.27       apply auto