remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc
authorhuffman
Thu, 23 Feb 2012 15:04:51 +0100
changeset 46607 6ae8121448af
parent 46606 7a5c05b5f945
child 46608 37e383cc7831
remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc
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