src/HOL/Old_Number_Theory/WilsonRuss.thy
 changeset 44766 d4d33a4d7548 parent 42793 88bee9f6eec7 child 44821 a92f65e174cf
```     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Sep 06 16:30:39 2011 -0700
1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Sep 06 19:03:41 2011 -0700
1.3 @@ -80,7 +80,7 @@
1.4  lemma inv_not_p_minus_1_aux:
1.5      "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
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.11    apply (subst dvd_minus_iff)
1.12 @@ -123,13 +123,13 @@
1.13      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
1.14    apply (subst int_int_eq [symmetric])
1.15    apply (simp add: zmult_int [symmetric])
1.16 -  apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
1.17 +  apply (simp add: left_diff_distrib right_diff_distrib)
1.18    done
1.19
1.20  lemma zcong_zpower_zmult:
1.21      "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
1.22    apply (induct z)