diff -r 9b403e123c1b -r 2740293cc458 List.ML --- 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];