diff -r 054ce38225b9 -r 87f6e8b93221 List.thy
--- 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)"