equal
deleted
inserted
replaced
10 *) |
10 *) |
11 |
11 |
12 atom_decl name |
12 atom_decl name |
13 atom_decl coname |
13 atom_decl coname |
14 |
14 |
15 ML {* val _ = cheat_alpha_eqvt := true *} |
|
16 ML {* val _ = cheat_equivp := true *} |
15 ML {* val _ = cheat_equivp := true *} |
17 ML {* val _ = cheat_fv_rsp := true *} |
|
18 |
16 |
19 nominal_datatype trm = |
17 nominal_datatype trm = |
20 Ax "name" "coname" |
18 Ax "name" "coname" |
21 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
19 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
22 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
20 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |