--- a/List.thy Fri Feb 11 11:09:50 1994 +0100
+++ b/List.thy Sat Feb 12 14:46:21 1994 +0100
@@ -58,6 +58,8 @@
"[x]" == "Cons(x, [])"
"[]" == "Nil"
+ "case xs of Nil => a | Cons(y,ys) => b" == "list_case(xs,a,%y ys.b)"
+
"[x:xs . P]" == "filter(%x.P,xs)"
"Alls x:xs.P" == "list_all(%x.P,xs)"