| changeset 16417 | 9bc16273c2d4 |
| parent 14065 | 8abaf978c9c2 |
| child 18241 | afdba6b3e383 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
4 Copyright 1995 TU Muenchen |
4 Copyright 1995 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* Basic definitions of Lambda-calculus *} |
7 header {* Basic definitions of Lambda-calculus *} |
8 |
8 |
9 theory Lambda = Main: |
9 theory Lambda imports Main begin |
10 |
10 |
11 |
11 |
12 subsection {* Lambda-terms in de Bruijn notation and substitution *} |
12 subsection {* Lambda-terms in de Bruijn notation and substitution *} |
13 |
13 |
14 datatype dB = |
14 datatype dB = |