src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 35048 82ab78fff970
parent 32960 69916a850301
child 35440 bdf8ad377877
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Feb 08 17:12:27 2010 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Feb 08 17:12:30 2010 +0100
@@ -82,9 +82,9 @@
 lemma inv_not_p_minus_1_aux:
     "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   apply (unfold zcong_def)
-  apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
+  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
-   apply (simp add: mult_commute)
+   apply (simp add: algebra_simps)
   apply (subst dvd_minus_iff)
   apply (subst zdvd_reduce)
   apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)