src/HOL/Library/Bit.thy
changeset 54489 03ff4d1e6784
parent 53063 8f7ac535892f
child 55416 dd7992d4a61a
--- a/src/HOL/Library/Bit.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Bit.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -147,11 +147,11 @@
 
 text {* All numerals reduce to either 0 or 1. *}
 
-lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
-  by (simp only: minus_one [symmetric] uminus_bit_def)
+lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
+  by (simp only: uminus_bit_def)
 
-lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
-  by (simp only: neg_numeral_def uminus_bit_def)
+lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
+  by (simp only: uminus_bit_def)
 
 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   by (simp only: numeral_Bit0 bit_add_self)