# HG changeset patch
# User huffman
# Date 1330005891 -3600
# Node ID 6ae8121448af0c10c7f5d88b5b7340a145691e65
# Parent  7a5c05b5f945e1d398d6c2d82083ada515748912
remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc

diff -r 7a5c05b5f945 -r 6ae8121448af src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 14:43:01 2012 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 15:04:51 2012 +0100
@@ -708,10 +708,6 @@
 lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
   by (simp add : no_sbintr m2pths)
 
-lemma bintrunc_Suc:
-  "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"
-  by (case_tac bin rule: bin_exhaust) auto
-
 lemma sign_Pls_ge_0: 
   "(bin_sign bin = 0) = (bin >= (0 :: int))"
   unfolding bin_sign_def by simp