| changeset 2898 | a95a497e1f4f |
| parent 2864 | bb647489f130 |
| child 2963 | 8b22497c25b9 |
| 2897:fd4fa6df22d1 | 2898:a95a497e1f4f |
|---|---|
1 header {* The Call-by-Value Lambda Calculus *} |
1 header {* The Call-by-Value Lambda Calculus *} |
2 theory Lt |
2 theory Lt |
3 imports Nominal2 |
3 imports "../../Nominal2" |
4 begin |
4 begin |
5 |
5 |
6 atom_decl name |
6 atom_decl name |
7 |
7 |
8 nominal_datatype lt = |
8 nominal_datatype lt = |