# HG changeset patch
# User huffman
# Date 1330100484 -3600
# Node ID 5ba230f8232f0dffa128559150606ed8ad08125d
# Parent  be76913ec1a4a6602ea8c638309b64a7e38d83a4
remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min

diff -r be76913ec1a4 -r 5ba230f8232f src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Feb 24 16:59:20 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 17:21:24 2012 +0100
@@ -1071,9 +1071,6 @@
   (eg) sint (number_of bin) on sint 1, must do
   (simp add: word_1_no del: numeral_1_eq_1) 
   *)
-lemma word_0_wi_Pls: "0 = word_of_int Int.Pls"
-  by (simp only: Pls_def word_0_wi)
-
 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
   by (simp add: word_number_of_alt)
 
@@ -1083,9 +1080,6 @@
 lemma word_m1_wi: "-1 = word_of_int -1" 
   by (rule word_number_of_alt)
 
-lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
-  by (simp add: word_m1_wi number_of_eq)
-
 lemma word_0_bl [simp]: "of_bl [] = 0"
   unfolding of_bl_def by simp
 
@@ -2140,8 +2134,6 @@
 
 lemmas bwsimps = 
   wi_hom_add
-  word_0_wi_Pls
-  word_m1_wi_Min
   word_wi_log_defs
 
 lemma word_bw_assocs:
@@ -2231,7 +2223,7 @@
   fixes x :: "'a::len0 word"
   shows "x + NOT x = -1"
   using word_of_int_Ex [where x=x] 
-  by (auto simp: bwsimps bin_add_not)
+  by (auto simp: bwsimps bin_add_not [unfolded Min_def])
 
 lemma word_plus_and_or [simp]:
   fixes x :: "'a::len0 word"