(* Title: HOL/Lambda/ListApplication.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TU MuenchenApplication 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