diff -r 201061643c4b -r 61b65ffb4186 List.ML
--- a/List.ML	Mon Oct 25 14:36:27 1993 +0100
+++ b/List.ML	Wed Nov 03 19:02:17 1993 +0100
@@ -310,6 +310,20 @@
 by (rtac list_rec_Cons 1);
 val list_case_Cons = result();
 
+(** @ - append **)
+
+goalw List.thy [append_def] "[]@xs = xs";
+by (rtac list_rec_Nil 1);
+val append_Nil = result();
+
+goalw List.thy [append_def] "Cons(x,xs)@ys = Cons(x,xs@ys)";
+by (rtac list_rec_Cons 1);
+val append_Cons = result();
+
+goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
+by(res_inst_tac [("l","xs")] list_induct 1);
+by(REPEAT(asm_simp_tac (list_ss addsimps [append_Nil,append_Cons]) 1));
+val append_assoc = result();
 
 (** The functional "map" **)