| changeset 2094 | 56b849d348ae |
| parent 2082 | 0854af516f14 |
| child 2104 | 2205b572bc9b |
| 2093:751d1349329b | 2094:56b849d348ae |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = cheat_supp_eq := true *} |
7 ML {* val _ = cheat_supp_eq := true *} |
8 ML {* val _ = cheat_equivp := true *} |
|
8 |
9 |
9 nominal_datatype lam = |
10 nominal_datatype lam = |
10 Var "name" |
11 Var "name" |
11 | App "lam" "lam" |
12 | App "lam" "lam" |
12 | Lam x::"name" t::"lam" bind_set x in t |
13 | Lam x::"name" t::"lam" bind_set x in t |