# HG changeset patch
# User huffman
# Date 1330006771 -3600
# Node ID 5cb607cb765198e860c9ed0ccd1fbf486f332eb6
# Parent  37e383cc78319d8b4ebd35cd3c1d0a7757e8cdd2
remove lemma bin_cat_Pls, which doesn't respect int/bin distinction

diff -r 37e383cc7831 -r 5cb607cb7651 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