src/HOL/Word/WordShift.thy
changeset 33640 0d82107dc07a
parent 33639 603320b93668
child 37604 1840dc0265da
     1.1 --- a/src/HOL/Word/WordShift.thy	Thu Nov 12 17:21:48 2009 +0100
     1.2 +++ b/src/HOL/Word/WordShift.thy	Thu Nov 12 17:21:51 2009 +0100
     1.3 @@ -1102,7 +1102,7 @@
     1.4     apply simp
     1.5    apply (rule bin_nth_rsplit)
     1.6       apply simp_all
     1.7 -  apply (simp add : word_size rev_map map_compose [symmetric])
     1.8 +  apply (simp add : word_size rev_map)
     1.9    apply (rule trans)
    1.10     defer
    1.11     apply (rule map_ident [THEN fun_cong])