| changeset 2328 | 10f699b48ba5 |
| parent 2327 | bcb037806e16 |
| child 2330 | 8728f7990f6d |
| 2327:bcb037806e16 | 2328:10f699b48ba5 |
|---|---|
1 theory SingleLet |
1 theory SingleLet |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
|
7 ML {* val _ = cheat_equivp := true *} |
|
8 |
6 |
9 nominal_datatype trm = |
7 nominal_datatype trm = |
10 Var "name" |
8 Var "name" |
11 | App "trm" "trm" |
9 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind_set x in t |
10 | Lam x::"name" t::"trm" bind_set x in t |