# HG changeset patch
# User huffman
# Date 1235666684 28800
# Node ID 419116f1157a41d66a13a4abcaa1c344f32936ee
# Parent  365ee7319b86d2d8b8706be785adf7a76ff8a24c
remove unnecessary simp rules

diff -r 365ee7319b86 -r 419116f1157a src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Thu Feb 26 08:44:12 2009 -0800
+++ b/src/HOL/Library/Bit.thy	Thu Feb 26 08:44:44 2009 -0800
@@ -79,14 +79,8 @@
 
 end
 
-lemma bit_1_plus_1 [simp]: "1 + 1 = (0 :: bit)"
-  unfolding plus_bit_def by simp
-
-lemma bit_add_self [simp]: "x + x = (0 :: bit)"
-  by (cases x) simp_all
-
-lemma bit_add_self_left [simp]: "x + (x + y) = (y :: bit)"
-  by simp
+lemma bit_add_self: "x + x = (0 :: bit)"
+  unfolding plus_bit_def by (simp split: bit.split)
 
 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
   unfolding times_bit_def by (simp split: bit.split)