author | paulson |
Thu, 01 Oct 1998 18:30:05 +0200 | |
changeset 5601 | b6456ccd9e3e |
parent 5261 | ce3c25c8a694 |
child 9102 | c7ba07e3bbe8 |
permissions | -rw-r--r-- |
5261 | 1 |
(* Title: HOL/Lambda/ListApplication.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TU Muenchen |
|
5 |
||
6 |
Application of a term to a list of terms |
|
7 |
*) |
|
8 |
||
9 |
ListApplication = Lambda + List + |
|
10 |
||
11 |
syntax "$$" :: dB => dB list => dB (infixl 150) |
|
12 |
translations "t $$ ts" == "foldl op$ t ts" |
|
13 |
||
14 |
end |