| changeset 2091 | 1f38489f1cf0 |
| parent 2082 | 0854af516f14 |
| child 2094 | 56b849d348ae |
| 2090:c00885a1534d | 2091:1f38489f1cf0 |
|---|---|
4 |
4 |
5 |
5 |
6 text {* example 3 or example 5 from Terms.thy *} |
6 text {* example 3 or example 5 from Terms.thy *} |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
9 |
|
10 ML {* val _ = cheat_alpha_eqvt := true *} |
|
11 ML {* val _ = cheat_equivp := true *} |
|
9 |
12 |
10 nominal_datatype trm = |
13 nominal_datatype trm = |
11 Vr "name" |
14 Vr "name" |
12 | Ap "trm" "trm" |
15 | Ap "trm" "trm" |
13 | Lm x::"name" t::"trm" bind_set x in t |
16 | Lm x::"name" t::"trm" bind_set x in t |