1.1 --- a/src/HOL/Library/Bit.thy	Thu Feb 26 08:44:12 2009 -0800
     1.2 +++ b/src/HOL/Library/Bit.thy	Thu Feb 26 08:44:44 2009 -0800
     1.3 @@ -79,14 +79,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma bit_1_plus_1 [simp]: "1 + 1 = (0 :: bit)"
     1.8 -  unfolding plus_bit_def by simp
     1.9 -
    1.10 -lemma bit_add_self [simp]: "x + x = (0 :: bit)"
    1.11 -  by (cases x) simp_all
    1.12 -
    1.13 -lemma bit_add_self_left [simp]: "x + (x + y) = (y :: bit)"
    1.14 -  by simp
    1.15 +lemma bit_add_self: "x + x = (0 :: bit)"
    1.16 +  unfolding plus_bit_def by (simp split: bit.split)
    1.17  
    1.18  lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
    1.19    unfolding times_bit_def by (simp split: bit.split)