# HG changeset patch
# User huffman
# Date 1332878321 -7200
# Node ID 3b5434efdf91717d88f58bae99a7f8ad496596d8
# Parent  e3e6c83efc39ee56977c7043b4529a045a3c45bf
remove unused premises

diff -r e3e6c83efc39 -r 3b5434efdf91 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 21:48:55 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 21:58:41 2012 +0200
@@ -613,8 +613,7 @@
 
 lemma sb_dec_lem:
   "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
-  by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
-    simplified zless2p, OF _ TrueI, simplified])
+  by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified])
 
 lemma sb_dec_lem':
   "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
diff -r e3e6c83efc39 -r 3b5434efdf91 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:48:55 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:58:41 2012 +0200
@@ -172,11 +172,11 @@
 
 lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
 
-lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
-  by (rule zmod_le_nonneg_dividend)
+lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
+  by (fact zmod_le_nonneg_dividend) (* FIXME: delete *)
 
-lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
-  by (rule int_mod_le [where a = "b - n" and n = n, simplified])
+lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n"
+  using zmod_le_nonneg_dividend [of "b - n" "n"] by simp
 
 lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
   apply (cases "0 <= a")