src/HOL/Old_Number_Theory/WilsonBij.thy
changeset 44766 d4d33a4d7548
parent 39159 0dec18004e75
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -75,7 +75,7 @@
     1.4  lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
     1.5    -- {* same as @{text WilsonRuss} *}
     1.6    apply (unfold zcong_def)
     1.7 -  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
     1.8 +  apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
     1.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    1.10     apply (simp add: algebra_simps)
    1.11    apply (subst dvd_minus_iff)
    1.12 @@ -213,7 +213,7 @@
    1.13  
    1.14  lemma reciP_sym: "zprime p ==> symP (reciR p)"
    1.15    apply (unfold reciR_def symP_def)
    1.16 -  apply (simp add: zmult_commute)
    1.17 +  apply (simp add: mult_commute)
    1.18    apply auto
    1.19    done
    1.20  
    1.21 @@ -240,7 +240,7 @@
    1.22      apply (subst setprod_insert)
    1.23        apply (auto simp add: fin_bijER)
    1.24    apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
    1.25 -   apply (simp add: zmult_assoc)
    1.26 +   apply (simp add: mult_assoc)
    1.27    apply (rule zcong_zmult)
    1.28     apply auto
    1.29    done