equal
deleted
inserted
replaced
310 |
310 |
311 Goalw [o_def] "map (f o g) xs = map f (map g xs)"; |
311 Goalw [o_def] "map (f o g) xs = map f (map g xs)"; |
312 by (induct_tac "xs" 1); |
312 by (induct_tac "xs" 1); |
313 by Auto_tac; |
313 by Auto_tac; |
314 qed "map_compose"; |
314 qed "map_compose"; |
315 Addsimps[map_compose]; |
315 (*Addsimps[map_compose];*) |
316 |
316 |
317 Goal "rev(map f xs) = map f (rev xs)"; |
317 Goal "rev(map f xs) = map f (rev xs)"; |
318 by (induct_tac "xs" 1); |
318 by (induct_tac "xs" 1); |
319 by Auto_tac; |
319 by Auto_tac; |
320 qed "rev_map"; |
320 qed "rev_map"; |