1.1 --- a/NEWS	Fri Dec 23 15:34:18 2011 +0100
     1.2 +++ b/NEWS	Fri Dec 23 15:55:23 2011 +0100
     1.3 @@ -84,6 +84,7 @@
     1.4    word_left_minus ~> left_minus
     1.5    word_diff_0_right ~> diff_0_right
     1.6    word_diff_self ~> diff_self
     1.7 +  word_sub_def ~> diff_minus
     1.8    word_diff_minus ~> diff_minus
     1.9    word_add_ac ~> add_ac
    1.10    word_mult_ac ~> mult_ac

     2.1 --- a/src/HOL/Word/Word.thy	Fri Dec 23 15:34:18 2011 +0100
     2.2 +++ b/src/HOL/Word/Word.thy	Fri Dec 23 15:55:23 2011 +0100
     2.3 @@ -247,10 +247,6 @@
     2.4  
     2.5  lemmas wi_hom_syms = wi_homs [symmetric]
     2.6  
     2.7 -lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
     2.8 -  unfolding word_sub_wi diff_minus
     2.9 -  by (simp only : word_uint.Rep_inverse wi_hom_syms)
    2.10 -
    2.11  lemma word_of_int_sub_hom:
    2.12    "(word_of_int a) - word_of_int b = word_of_int (a - b)"
    2.13    by (simp add: word_sub_wi arths)