--- a/List.ML Wed Feb 08 14:06:37 1995 +0100
+++ b/List.ML Mon Feb 13 15:12:08 1995 +0100
@@ -34,6 +34,7 @@
mem_Nil, mem_Cons,
append_Nil, append_Cons,
map_Nil, map_Cons,
+ flat_Nil, flat_Cons,
list_all_Nil, list_all_Cons,
filter_Nil, filter_Cons];
@@ -109,6 +110,13 @@
bind_thm("list_eq_cases",
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
+(** flat **)
+
+goal List.thy "flat(xs@ys) = flat(xs)@flat(ys)";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc])));
+qed"flat_append";
+
(** nth **)
val [nth_0,nth_Suc] = nat_recs nth_def;
@@ -136,5 +144,5 @@
[not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
mem_append, mem_filter,
map_ident, map_append, map_compose,
- list_all_True, list_all_conj, nth_0, nth_Suc];
+ flat_append, list_all_True, list_all_conj, nth_0, nth_Suc];