--- a/List.ML Fri Jun 17 18:28:36 1994 +0200
+++ b/List.ML Fri Jun 17 18:30:18 1994 +0200
@@ -407,6 +407,16 @@
by (ALLGOALS (asm_simp_tac map_ss));
val map_ident = result();
+goal List.thy "map(f, xs@ys) = map(f,xs) @ map(f,ys)";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (map_ss addsimps [append_Nil,append_Cons])));
+val map_append = result();
+
+goalw List.thy [o_def] "map(f o g, xs) = map(f, map(g, xs))";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac map_ss));
+val map_compose = result();
+
goal List.thy "!!f. (!!x. f(x): Sexp) ==> \
\ Abs_map(g, Rep_map(f,xs)) = map(%t. g(f(t)), xs)";
by (list_ind_tac "xs" 1);