src/HOL/NumberTheory/IntPrimes.thy
changeset 14271 8ed6989228bb
parent 14174 f3cafd2929d5
child 14353 79f9fbef9106
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Dec 02 11:48:15 2003 +0100
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed Dec 03 10:49:34 2003 +0100
     1.3 @@ -305,7 +305,7 @@
     1.4     apply (rule_tac [!] zrelprime_zdvd_zmult)
     1.5       apply (simp_all add: zdiff_zmult_distrib)
     1.6    apply (subgoal_tac "m dvd (-(a * k - b * k))")
     1.7 -   apply (simp add: zminus_zdiff_eq)
     1.8 +   apply simp
     1.9    apply (subst zdvd_zminus_iff, assumption)
    1.10    done
    1.11  
    1.12 @@ -380,7 +380,7 @@
    1.13    apply (unfold zcong_def dvd_def)
    1.14    apply (rule_tac x = "a mod m" in exI, auto)
    1.15    apply (rule_tac x = "-(a div m)" in exI)
    1.16 -  apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
    1.17 +  apply (simp add: diff_eq_eq eq_diff_eq add_commute)
    1.18    done
    1.19  
    1.20  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
    1.21 @@ -395,7 +395,7 @@
    1.22  
    1.23  lemma zcong_zmod_aux:
    1.24       "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
    1.25 -  by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
    1.26 +  by(simp add: zdiff_zmult_distrib2 add_diff_eq eq_diff_eq add_ac)
    1.27  
    1.28  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
    1.29    apply (unfold zcong_def)
    1.30 @@ -505,7 +505,7 @@
    1.31      ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
    1.32    apply (rule trans)
    1.33     apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
    1.34 -  apply (simp add: eq_zdiff_eq zmult_commute)
    1.35 +  apply (simp add: eq_diff_eq mult_commute)
    1.36    done
    1.37  
    1.38  lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"