src/HOL/Word/BinBoolList.thy
changeset 31790 05c92381363c
parent 30971 7fbebf75b3ef
child 32439 7a91c7bcfe7e
     1.1 --- a/src/HOL/Word/BinBoolList.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Word/BinBoolList.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -658,7 +658,7 @@
     1.4    apply (unfold bl_to_bin_def)
     1.5    apply (induct n)
     1.6     apply simp
     1.7 -  apply (simp only: Suc_eq_add_numeral_1 replicate_add
     1.8 +  apply (simp only: Suc_eq_plus1 replicate_add
     1.9                      append_Cons [symmetric] bl_to_bin_aux_append)
    1.10    apply simp
    1.11    done