equal
deleted
inserted
replaced
11 |
11 |
12 atom_decl name |
12 atom_decl name |
13 atom_decl coname |
13 atom_decl coname |
14 |
14 |
15 ML {* val _ = cheat_equivp := true *} |
15 ML {* val _ = cheat_equivp := true *} |
16 ML {* val _ = cheat_fv_rsp := true *} |
|
17 |
16 |
18 nominal_datatype trm = |
17 nominal_datatype trm = |
19 Ax "name" "coname" |
18 Ax "name" "coname" |
20 | 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 |
21 | 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 |