--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Feb 08 17:12:27 2010 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Feb 08 17:12:30 2010 +0100
@@ -74,9 +74,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: 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)
--- 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)
--- a/src/HOL/Word/BinGeneral.thy Mon Feb 08 17:12:27 2010 +0100
+++ b/src/HOL/Word/BinGeneral.thy Mon Feb 08 17:12:30 2010 +0100
@@ -742,7 +742,7 @@
lemma sb_inc_lem':
"(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
- by (rule iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0])
+ by (rule sb_inc_lem) simp
lemma sbintrunc_inc:
"x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"