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