diff -r 201061643c4b -r 61b65ffb4186 List.thy
--- a/List.thy	Mon Oct 25 14:36:27 1993 +0100
+++ b/List.thy	Wed Nov 03 19:02:17 1993 +0100
@@ -39,6 +39,7 @@
   tl            :: "'a list => 'a list"
   list_all      :: "('a => bool) => ('a list => bool)"
   map           :: "('a=>'b) => ('a list => 'b list)"
+  "@"		:: "['a list, 'a list] => 'a list"		(infixr 65)
   list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
 
   (* List Enumeration *)
@@ -98,7 +99,7 @@
   tl_def        "tl(xs)              == list_rec(xs, @xs.True, %x xs r.xs)"
   list_all_def  "list_all(P, xs)     == list_rec(xs, True, %x l r. P(x) & r)"
   map_def       "map(f, xs)          == list_rec(xs, Nil, %x l r. Cons(f(x), r))"
+  append_def	"xs@ys               == list_rec(xs, ys, %x l r. Cons(x,r))"
   list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
 
 end
-