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])