# HG changeset patch
# User huffman
# Date 1323773339 -3600
# Node ID 6374cd925b185b29c38b34567b4094c4f242bc19
# Parent  c58ce659ce2aed16592357c3d1863c93c5e9b2dc
remove redundant lemmas

diff -r c58ce659ce2a -r 6374cd925b18 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 11:26:10 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 11:48:59 2011 +0100
@@ -54,12 +54,6 @@
 
 lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
 
-lemma Min_ne_Pls [iff]:  
-  "Int.Min ~= Int.Pls"
-  unfolding Min_def Pls_def by auto
-
-lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
-
 lemmas PlsMin_defs [intro!] = 
   Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]