# HG changeset patch
# User huffman
# Date 1332877735 -7200
# Node ID e3e6c83efc39ee56977c7043b4529a045a3c45bf
# Parent  8395d7d63fc8a2dee6dc8912ce6b46335f723d64
remove duplicate lemmas

diff -r 8395d7d63fc8 -r e3e6c83efc39 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:48:26 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:48:55 2012 +0200
@@ -96,26 +96,10 @@
 
 lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2]]
 
-lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b"
-  by (fact zminus_zmod) (* FIXME: delete *)
-
-lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
-  by (fact mod_diff_eq) (* FIXME: delete *)
-
-lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
-  by (fact mod_diff_right_eq) (* FIXME: delete *)
-
-lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
-  by (fact mod_diff_left_eq) (* FIXME: delete *)
-
 lemma zmod_zsub_self [simp]: 
   "((b :: int) - a) mod a = b mod a"
   by (simp add: mod_diff_right_eq)
 
-lemma zmod_zmult1_eq_rev:
-  "b * a mod c = b mod c * a mod (c::int)"
-  by (fact mod_mult_left_eq) (* FIXME: delete *)
-
 lemmas rdmods [symmetric] = mod_minus_eq
   mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
   mod_add_right_eq mod_mult_right_eq mod_mult_left_eq