# HG changeset patch
# User huffman
# Date 1329992694 -3600
# Node ID 102a06189a6c9e6d99f80b4962915e627bcca183
# Parent  fd0ac848140e724ddccd9e5771ba7ca549496e14
remove lemmas Bit{0,1}_div2

diff -r fd0ac848140e -r 102a06189a6c src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 11:20:42 2012 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 11:24:54 2012 +0100
@@ -223,12 +223,6 @@
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   unfolding bin_rest_def [symmetric] by auto
 
-lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
-  using Bit_div2 [where b="(0::bit)"] by (simp add: BIT_simps)
-
-lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
-  using Bit_div2 [where b="(1::bit)"] by (simp add: BIT_simps)
-
 lemma bin_nth_lem [rule_format]:
   "ALL y. bin_nth x = bin_nth y --> x = y"
   apply (induct x rule: bin_induct)