# HG changeset patch
# User huffman
# Date 1324652123 -3600
# Node ID 43eac86bf00681980518168aee17a31633a9737b
# Parent  ae70b6830f1517c55eca43f7b21c8db9c61b3b9d
remove redundant lemma word_sub_def

diff -r ae70b6830f15 -r 43eac86bf006 NEWS
--- a/NEWS	Fri Dec 23 15:34:18 2011 +0100
+++ b/NEWS	Fri Dec 23 15:55:23 2011 +0100
@@ -84,6 +84,7 @@
   word_left_minus ~> left_minus
   word_diff_0_right ~> diff_0_right
   word_diff_self ~> diff_self
+  word_sub_def ~> diff_minus
   word_diff_minus ~> diff_minus
   word_add_ac ~> add_ac
   word_mult_ac ~> mult_ac
diff -r ae70b6830f15 -r 43eac86bf006 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Dec 23 15:34:18 2011 +0100
+++ b/src/HOL/Word/Word.thy	Fri Dec 23 15:55:23 2011 +0100
@@ -247,10 +247,6 @@
 
 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)