src/HOL/NumberTheory/Chinese.thy
changeset 13187 e5434b822a96
parent 11868 56db9f3a6b3e
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Thu May 30 10:12:11 2002 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Thu May 30 10:12:52 2002 +0200
     1.3 @@ -185,14 +185,11 @@
     1.4       apply (rule_tac [!] funprod_zgcd)
     1.5       apply safe
     1.6       apply simp_all
     1.7 -    apply (subgoal_tac [3] "ia \<le> n")
     1.8 -     prefer 4
     1.9 -     apply arith
    1.10 -     apply (subgoal_tac "i<n")
    1.11 -     prefer 2
    1.12 -     apply arith
    1.13 -    apply (case_tac [2] i)
    1.14 -     apply simp_all
    1.15 +   apply (subgoal_tac "i<n")
    1.16 +    prefer 2
    1.17 +    apply arith
    1.18 +   apply (case_tac [2] i)
    1.19 +    apply simp_all
    1.20    done
    1.21  
    1.22  lemma aux: