diff -r 70d46a081b47 -r 7d437bed7765 List.thy
--- a/List.thy	Fri Jan 14 12:35:27 1994 +0100
+++ b/List.thy	Mon Jan 24 15:59:02 1994 +0100
@@ -37,22 +37,29 @@
   null          :: "'a list => bool"
   hd            :: "'a list => 'a"
   tl            :: "'a list => 'a list"
+  mem		:: "['a, 'a list] => bool"			(infixl 55)
   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"
+  filter	:: "['a => bool, 'a list] => 'a list"
 
   (* List Enumeration *)
 
   "[]"          :: "'a list"                            ("[]")
   "@List"       :: "args => 'a list"                    ("[(_)]")
 
+  (* Special syntax for list_all and filter *)
+  "@Alls"	:: "[id, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
+  "@filter"	:: "[id, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
 
 translations
   "[x, xs]"     == "Cons(x, [xs])"
   "[x]"         == "Cons(x, [])"
   "[]"          == "Nil"
 
+  "[x:xs . P]"	== "filter(%x.P,xs)"
+  "Alls x:xs.P"	== "list_all(%x.P,xs)"
 
 rules
 
@@ -97,9 +104,13 @@
   null_def      "null(xs)            == list_rec(xs, True, %x xs r.False)"
   hd_def        "hd(xs)              == list_rec(xs, @x.True, %x xs r.x)"
   tl_def        "tl(xs)              == list_rec(xs, @xs.True, %x xs r.xs)"
+  mem_def	"x mem xs            == \
+\		   list_rec(xs, False, %y ys r. if(y=x, True, r))"
   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))"
+  map_def       "map(f, xs)          == list_rec(xs, [], %x l r. Cons(f(x),r))"
   append_def	"xs@ys               == list_rec(xs, ys, %x l r. Cons(x,r))"
+  filter_def	"filter(P,xs)        == \
+\                  list_rec(xs, [], %x xs r. if(P(x), Cons(x,r), r))"
   list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
 
 end