--- a/src/HOL/NumberTheory/WilsonBij.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.thy Wed Dec 03 10:49:34 2003 +0100
@@ -75,9 +75,9 @@
lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
-- {* same as @{text WilsonRuss} *}
apply (unfold zcong_def)
- apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
+ apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
- apply (simp add: zmult_commute zminus_zdiff_eq)
+ apply (simp add: mult_commute)
apply (subst zdvd_zminus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)