remove lemma bin_cat_Pls, which doesn't respect int/bin distinction
authorhuffman
Thu, 23 Feb 2012 15:19:31 +0100
changeset 46609 5cb607cb7651
parent 46608 37e383cc7831
child 46610 0c3a5e28f425
remove lemma bin_cat_Pls, which doesn't respect int/bin distinction
src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Thu Feb 23 15:15:48 2012 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Thu Feb 23 15:19:31 2012 +0100
@@ -488,9 +488,6 @@
 lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
   by (induct n arbitrary: w) auto
 
-lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
-  unfolding Pls_def by (rule bin_cat_zero)
-
 lemma bintr_cat1: 
   "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   by (induct n arbitrary: b) auto