src/HOL/Word/Word.thy

   wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
   wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
   by (auto simp: word_arith_wis arths)
 
 lemmas wi_hom_syms = wi_homs [symmetric]
-
-lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
-  unfolding word_sub_wi diff_minus
-  by (simp only : word_uint.Rep_inverse wi_hom_syms)
 
 lemma word_of_int_sub_hom:
   "(word_of_int a) - word_of_int b = word_of_int (a - b)"
   by (simp add: word_sub_wi arths)