| changeset 2649 | a8ebcb368a15 |
| parent 2645 | 09cf78bb53d4 |
| child 2654 | 0f0335d91456 |
| 2648:5d9724ad543d | 2649:a8ebcb368a15 |
|---|---|
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 atom_decl name |
6 atom_decl name |
7 |
|
8 ML {* suffix *} |
|
7 |
9 |
8 nominal_datatype lam = |
10 nominal_datatype lam = |
9 Var "name" |
11 Var "name" |
10 | App "lam" "lam" |
12 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l |
13 | Lam x::"name" l::"lam" bind x in l |