--- 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
-