# HG changeset patch
# User haftmann
# Date 1265645550 -3600
# Node ID 82ab78fff9708c9cc1f5f367999cf9f234a30457
# Parent  1b2bae06c7962d37cf6c736cced71bb63b8b880f
tuned proofs

diff -r 1b2bae06c796 -r 82ab78fff970 src/HOL/Old_Number_Theory/WilsonBij.thy
--- 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)
diff -r 1b2bae06c796 -r 82ab78fff970 src/HOL/Old_Number_Theory/WilsonRuss.thy
--- 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)
diff -r 1b2bae06c796 -r 82ab78fff970 src/HOL/Word/BinGeneral.thy
--- 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"