# HG changeset patch
# User huffman
# Date 1325006775 -3600
# Node ID 5cb7ef5bfef21b15ce36c2ff23ce1642ab838a27
# Parent  b319f1b0c6341ea432c39279209d94fcfb3baa93
remove duplicate lemma lists

diff -r b319f1b0c634 -r 5cb7ef5bfef2 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Dec 27 15:38:45 2011 +0100
+++ b/src/HOL/Word/Word.thy	Tue Dec 27 18:26:15 2011 +0100
@@ -249,16 +249,10 @@
   "(word_of_int a) - word_of_int b = word_of_int (a - b)"
   by (simp add: word_sub_wi arths)
 
-lemmas new_word_of_int_homs = 
-  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
-
-lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
-
-lemmas word_of_int_hom_syms =
-  new_word_of_int_hom_syms (* FIXME: duplicate *)
-
 lemmas word_of_int_homs =
-  new_word_of_int_homs (* FIXME: duplicate *)
+  word_of_int_sub_hom wi_homs word_0_wi word_1_wi
+
+lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
 
 (* FIXME: provide only one copy of these theorems! *)
 lemmas word_of_int_add_hom = wi_hom_add
@@ -1204,7 +1198,7 @@
   by (rule word_uint.Abs_cases [of b],
       rule word_uint.Abs_cases [of a],
       simp add: add_commute mult_commute 
-                ring_distribs new_word_of_int_homs
+                ring_distribs word_of_int_homs
            del: word_of_int_0 word_of_int_1)+
 
 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
@@ -1237,7 +1231,7 @@
   "word_succ (number_of bin) = number_of (Int.succ bin) & 
     word_pred (number_of bin) = number_of (Int.pred bin)"
   unfolding word_number_of_def Int.succ_def Int.pred_def
-  by (simp add: new_word_of_int_homs)
+  by (simp add: word_of_int_homs)
 
 lemma word_sp_01 [simp] : 
   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
@@ -3152,7 +3146,7 @@
   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
-  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
+  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
 
 lemma mask_power_eq:
   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
@@ -3448,7 +3442,7 @@
   "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
   apply (unfold of_bl_def)
   apply (simp add: bl_to_bin_app_cat bin_cat_num)
-  apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
+  apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
   done
 
 lemma of_bl_False [simp]: