src/HOL/Word/Word.thy

   apply (clarsimp simp add : uno_simps)
   done
 
 lemma word_of_int_power_hom: 
   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
-  by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
+  by (induct n) (simp_all add: word_of_int_hom_syms)
 
 lemma word_arith_power_alt: 
   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
   by (simp add : word_of_int_power_hom [symmetric])
 

   fixes x :: "'a::len0 word"
   shows "(x OR y) AND z = x AND z OR y AND z"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]   
-  by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
+  by (auto simp: bwsimps bbw_ao_dist)
 
 lemma word_oa_dist:
   fixes x :: "'a::len0 word"
   shows "x AND y OR z = (x OR z) AND (y OR z)"
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]   
-  by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
+  by (auto simp: bwsimps bbw_oa_dist)
 
 lemma word_add_not [simp]: 
   fixes x :: "'a::len0 word"
   shows "x + NOT x = -1"
   using word_of_int_Ex [where x=x] 

     
 lemma word_set_set_diff: 
   fixes w :: "'a::len0 word"
   assumes "m ~= n"
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
-  by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
+  by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
     
 lemma test_bit_no': 
   fixes w :: "'a::len0 word"
   shows "w = number_of bin \<Longrightarrow> test_bit w n = (n < size w & bin_nth bin n)"
   unfolding word_test_bit_def word_number_of_def word_size

   apply (clarsimp simp add: word_size test_bit_no)
   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
   done
 
 lemma word_msb_n1: "msb (-1::'a::len word)"
-  unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
+  unfolding word_msb_alt to_bl_n1 by simp
 
 declare word_set_set_same [simp] word_set_nth [simp]
   test_bit_no [simp] word_set_no [simp] nth_0 [simp]
   setBit_no [simp] clearBit_no [simp]
   word_lsb_no [simp] word_msb_no [simp] word_msb_n1 [simp] word_lsb_1_0 [simp]

   apply simp
   done
 
 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   unfolding shiftl_def 
-  by (induct n) (auto simp: shiftl1_2t power_Suc)
+  by (induct n) (auto simp: shiftl1_2t)
 
 lemma shiftr1_bintr [simp]:
   "(shiftr1 (number_of w) :: 'a :: len0 word) = 
     number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" 
   unfolding shiftr1_def word_number_of_def

   apply (rule trans)
    apply (rule test_bit_rsplit_alt)
      apply (clarsimp simp: word_size)+
   apply (rule trans)
   apply (rule test_bit_rcat [OF refl refl])
-  apply (simp add : word_size msrevs)
+  apply (simp add: word_size msrevs)
   apply (subst nth_rev)
    apply arith
-  apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
+  apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
   apply safe
-  apply (simp add : diff_mult_distrib)
+  apply (simp add: diff_mult_distrib)
   apply (rule mpl_lem)
   apply (cases "size ws")
    apply simp_all
   done