--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListApplication.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/Lambda/ListApplication.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Application of a term to a list of terms
+*)
+
+ListApplication = Lambda + List +
+
+syntax "$$" :: dB => dB list => dB (infixl 150)
+translations "t $$ ts" == "foldl op$ t ts"
+
+end