src/HOL/NumberTheory/Chinese.thy
changeset 20272 0ca998e83447
parent 19670 2e4a143c73c5
child 20432 07ec57376051
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Jul 31 20:56:49 2006 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Mon Jul 31 21:06:40 2006 +0200
     1.3 @@ -175,11 +175,6 @@
     1.4       apply (rule_tac [!] funprod_zgcd)
     1.5       apply safe
     1.6       apply simp_all
     1.7 -   apply (subgoal_tac "i<n")
     1.8 -    prefer 2
     1.9 -    apply arith
    1.10 -   apply (case_tac [2] i)
    1.11 -    apply simp_all
    1.12    done
    1.13  
    1.14  lemma x_sol_lin_aux: