| changeset 1445 | 3246c5e1a9d7 |
| parent 1441 | 14b850159df1 |
| child 1447 | 378b8c791de8 |
| 1444:aca9a6380c3f | 1445:3246c5e1a9d7 |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 text {* example 1, equivalent to example 2 from Terms *} |
5 text {* example 1, equivalent to example 2 from Terms *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
|
9 ML {* val cheat_alpha_eqvt = ref false *} |
|
8 |
10 |
9 nominal_datatype lam = |
11 nominal_datatype lam = |
10 VAR "name" |
12 VAR "name" |
11 | APP "lam" "lam" |
13 | APP "lam" "lam" |
12 | LET bp::"bp" t::"lam" bind "bi bp" in t |
14 | LET bp::"bp" t::"lam" bind "bi bp" in t |