# HG changeset patch
# User huffman
# Date 1324986543 -3600
# Node ID cce7e6197a46b905e30e9b17c3ec98bcf348fcb1
# Parent  d7cc533ae60df6f458859fc6283ae56dcdd8c5d1
removed unused lemmas

diff -r d7cc533ae60d -r cce7e6197a46 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 12:37:11 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 12:49:03 2011 +0100
@@ -561,11 +561,6 @@
 lemmas bintrunc_Min_minus_I = bmsts(2)
 lemmas bintrunc_BIT_minus_I = bmsts(3)
 
-lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
-  by (fact bintrunc.Z) (* FIXME: delete *)
-lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
-  by (fact bintrunc.Z) (* FIXME: delete *)
-
 lemma bintrunc_Suc_lem:
   "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
   by auto