equal
deleted
inserted
replaced
1 (* Title: HOL/Proofs/Lambda/ListApplication.thy |
1 (* Title: HOL/Proofs/Lambda/ListApplication.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 1998 TU Muenchen |
3 Copyright 1998 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Application of a term to a list of terms *} |
6 section {* Application of a term to a list of terms *} |
7 |
7 |
8 theory ListApplication imports Lambda begin |
8 theory ListApplication imports Lambda begin |
9 |
9 |
10 abbreviation |
10 abbreviation |
11 list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) where |
11 list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) where |