--- a/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 28 17:51:54 2013 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 28 21:06:22 2013 +0100
@@ -253,14 +253,6 @@
"(x :: nat) < z ==> (x - y) mod z = x - y"
by (rule nat_mod_eq') arith
-lemma int_mod_lem:
- "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
- apply safe
- apply (erule (1) mod_pos_pos_trivial)
- apply (erule_tac [!] subst)
- apply auto
- done
-
lemma int_mod_eq:
"(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
by clarsimp (rule mod_pos_pos_trivial)