diff -r c533bc92e882 -r d465d3be2744 List.ML
--- a/List.ML	Wed Dec 14 11:17:18 1994 +0100
+++ b/List.ML	Thu Jan 26 10:41:21 1995 +0100
@@ -50,6 +50,11 @@
 by(ALLGOALS(asm_simp_tac list_ss));
 qed "append_Nil2";
 
+goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+qed "append_is_Nil";
+
 (** mem **)
 
 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
@@ -91,6 +96,11 @@
 by(fast_tac HOL_cs 1);
 qed "expand_list_case";
 
+(** nth **)
+
+val [nth_0,nth_Suc] = nat_recs nth_def; 
+store_thm("nth_0",nth_0);
+store_thm("nth_Suc",nth_Suc);
 
 (** Additional mapping lemmas **)
 
@@ -110,7 +120,8 @@
 qed "map_compose";
 
 val list_ss = list_ss addsimps
-  [not_Cons_self, append_assoc, append_Nil2, mem_append, mem_filter,
+  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil,
+   mem_append, mem_filter,
    map_ident, map_append, map_compose,
-   list_all_True, list_all_conj];
+   list_all_True, list_all_conj, nth_0, nth_Suc];