src/HOL/NumberTheory/Chinese.thy
changeset 13187 e5434b822a96
parent 11868 56db9f3a6b3e
child 13524 604d0f3622d6
--- a/src/HOL/NumberTheory/Chinese.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Thu May 30 10:12:52 2002 +0200
@@ -185,14 +185,11 @@
      apply (rule_tac [!] funprod_zgcd)
      apply safe
      apply simp_all
-    apply (subgoal_tac [3] "ia \<le> n")
-     prefer 4
-     apply arith
-     apply (subgoal_tac "i<n")
-     prefer 2
-     apply arith
-    apply (case_tac [2] i)
-     apply simp_all
+   apply (subgoal_tac "i<n")
+    prefer 2
+    apply arith
+   apply (case_tac [2] i)
+    apply simp_all
   done
 
 lemma aux: