| changeset 2030 | 43d7612f1429 |
| parent 2026 | 7f504136149b |
| child 2082 | 0854af516f14 |
| 2029:e72121ea134b | 2030:43d7612f1429 |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 text {* example 2 *} |
5 text {* example 2 *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
|
9 ML {* val _ = cheat_alpha_eqvt := true *} |
|
10 |
8 |
11 nominal_datatype trm = |
9 nominal_datatype trm = |
12 Var "name" |
10 Var "name" |
13 | App "trm" "trm" |
11 | App "trm" "trm" |
14 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |