equal
deleted
inserted
replaced
3 Copyright 1995 TU Muenchen |
3 Copyright 1995 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Basic definitions of Lambda-calculus *} |
6 header {* Basic definitions of Lambda-calculus *} |
7 |
7 |
8 theory Lambda imports Main begin |
8 theory Lambda |
|
9 imports Old_Datatype |
|
10 begin |
9 |
11 |
10 declare [[syntax_ambiguity_warning = false]] |
12 declare [[syntax_ambiguity_warning = false]] |
11 |
13 |
12 |
14 |
13 subsection {* Lambda-terms in de Bruijn notation and substitution *} |
15 subsection {* Lambda-terms in de Bruijn notation and substitution *} |