# HG changeset patch
# User huffman
# Date 1323438771 -3600
# Node ID 3a3e4c58083c10042c387db78c3f07d2ead2c9b4
# Parent  fe44c0b216efd72f9d2a66c1074143fe2a81cb37
remove redundant lemma word_diff_minus

diff -r fe44c0b216ef -r 3a3e4c58083c NEWS
--- a/NEWS	Fri Dec 09 14:14:05 2011 +0100
+++ b/NEWS	Fri Dec 09 14:52:51 2011 +0100
@@ -80,6 +80,7 @@
   word_left_minus ~> left_minus
   word_diff_0_right ~> diff_0_right
   word_diff_self ~> diff_self
+  word_diff_minus ~> diff_minus
   word_add_ac ~> add_ac
   word_mult_ac ~> mult_ac
   word_plus_ac0 ~> add_0_left add_0_right add_ac
diff -r fe44c0b216ef -r 3a3e4c58083c src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Dec 09 14:14:05 2011 +0100
+++ b/src/HOL/Word/Word.thy	Fri Dec 09 14:52:51 2011 +0100
@@ -249,8 +249,6 @@
 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)
-    
-lemmas word_diff_minus = word_sub_def
 
 lemma word_of_int_sub_hom:
   "(word_of_int a) - word_of_int b = word_of_int (a - b)"