--- a/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 17 15:22:14 2016 +0100
@@ -201,10 +201,6 @@
lemmas push_mods = push_mods' [THEN eq_reflection]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
-lemmas mod_simps =
- mod_mult_self2_is_0 [THEN eq_reflection]
- mod_mult_self1_is_0 [THEN eq_reflection]
- mod_mod_trivial [THEN eq_reflection]
lemma nat_mod_eq:
"!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"