# HG changeset patch
# User huffman
# Date 1330004581 -3600
# Node ID 7a5c05b5f945e1d398d6c2d82083ada515748912
# Parent  b2563f7cf84459544b5f88f274d0d346d101e2fd
remove unused lemmas

diff -r b2563f7cf844 -r 7a5c05b5f945 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 14:29:29 2012 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 14:43:01 2012 +0100
@@ -111,12 +111,6 @@
   apply (simp add: z1pmod2)
   done
 
-lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
-  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
-
-lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
-  unfolding numeral_simps number_of_is_id by simp
-
 lemma neB1E [elim!]:
   assumes ne: "y \<noteq> (1::bit)"
   assumes y: "y = (0::bit) \<Longrightarrow> P"