1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -90,10 +90,8 @@
     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 [1] zdvd_zmult2)
     1.8 -    apply (rule_tac [2] zdvd_zmult)
     1.9 -    apply (subgoal_tac "i = Suc (k + l)")
    1.10 -    apply (simp_all (no_asm_simp))
    1.11 +  apply (subgoal_tac "i = Suc (k + l)")
    1.12 +   apply (simp_all (no_asm_simp))
    1.13    done
    1.14  
    1.15  lemma funsum_mod:
    1.16 @@ -103,7 +101,7 @@
    1.17    apply (rule trans)
    1.18     apply (rule mod_add_eq)
    1.19    apply simp
    1.20 -  apply (rule zmod_zadd_right_eq [symmetric])
    1.21 +  apply (rule mod_add_right_eq [symmetric])
    1.22    done
    1.23  
    1.24  lemma funsum_zero [rule_format (no_asm)]:
    1.25 @@ -196,8 +194,8 @@
    1.26     apply (case_tac [2] "i = n")
    1.27      apply (simp_all (no_asm_simp))
    1.28      apply (case_tac [3] "j < i")
    1.29 -     apply (rule_tac [3] zdvd_zmult2)
    1.30 -     apply (rule_tac [4] zdvd_zmult)
    1.31 +     apply (rule_tac [3] dvd_mult2)
    1.32 +     apply (rule_tac [4] dvd_mult)
    1.33       apply (rule_tac [!] funprod_zdvd)
    1.34       apply arith
    1.35       apply arith
    1.36 @@ -217,8 +215,8 @@
    1.37    apply (subst funsum_mod)
    1.38    apply (subst funsum_oneelem)
    1.39       apply auto
    1.40 -  apply (subst zdvd_iff_zmod_eq_0 [symmetric])
    1.41 -  apply (rule zdvd_zmult)
    1.42 +  apply (subst dvd_eq_mod_eq_0 [symmetric])
    1.43 +  apply (rule dvd_mult)
    1.44    apply (rule x_sol_lin_aux)
    1.45    apply auto
    1.46    done
    1.47 @@ -238,20 +236,20 @@
    1.48    apply safe
    1.49      apply (tactic {* stac (thm "zcong_zmod") 3 *})
    1.50      apply (tactic {* stac (thm "mod_mult_eq") 3 *})
    1.51 -    apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
    1.52 -      apply (tactic {* stac (thm "x_sol_lin") 5 *})
    1.53 -        apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
    1.54 -        apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
    1.55 -        apply (subgoal_tac [7]
    1.56 +    apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
    1.57 +      apply (tactic {* stac (thm "x_sol_lin") 4 *})
    1.58 +        apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
    1.59 +        apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
    1.60 +        apply (subgoal_tac [6]
    1.61            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
    1.62            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
    1.63 -         prefer 7
    1.64 +         prefer 6
    1.65           apply (simp add: zmult_ac)
    1.66          apply (unfold xilin_sol_def)
    1.67 -        apply (tactic {* asm_simp_tac @{simpset} 7 *})
    1.68 -        apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
    1.69 -        apply (rule_tac [7] unique_xi_sol)
    1.70 -           apply (rule_tac [4] funprod_zdvd)
    1.71 +        apply (tactic {* asm_simp_tac @{simpset} 6 *})
    1.72 +        apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
    1.73 +        apply (rule_tac [6] unique_xi_sol)
    1.74 +           apply (rule_tac [3] funprod_zdvd)
    1.75              apply (unfold m_cond_def)
    1.76              apply (rule funprod_pos [THEN pos_mod_sign])
    1.77              apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])