1.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Tue May 11 20:11:08 2004 +0200
     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: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
     1.8 +  apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
     1.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    1.10     apply (simp add: mult_commute)
    1.11    apply (subst zdvd_zminus_iff)