diff -r de514a98f6b6 -r 689ebcbd6343 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Feb 24 13:37:23 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 13:50:37 2012 +0100
@@ -1086,19 +1086,17 @@
 lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
   by (simp add: word_m1_wi number_of_eq)
 
-lemma word_0_bl [simp]: "of_bl [] = 0" 
-  unfolding of_bl_def by (simp add: Pls_def)
+lemma word_0_bl [simp]: "of_bl [] = 0"
+  unfolding of_bl_def by simp
 
 lemma word_1_bl: "of_bl [True] = 1" 
-  unfolding of_bl_def
-  by (simp add: bl_to_bin_def Bit_def Pls_def)
-
-lemma uint_eq_0 [simp] : "(uint 0 = 0)" 
-  unfolding word_0_wi
-  by (simp add: word_ubin.eq_norm Pls_def [symmetric])
+  unfolding of_bl_def by (simp add: bl_to_bin_def)
+
+lemma uint_eq_0 [simp]: "uint 0 = 0"
+  unfolding word_0_wi word_ubin.eq_norm by simp
 
 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
-  by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
+  by (simp add: of_bl_def bl_to_bin_rep_False)
 
 lemma to_bl_0 [simp]:
   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"