equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 (* example 6 from Peter Sewell's bestiary *) |
5 (* example 6 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
|
8 |
|
9 (* The binding structure is too complicated, so we cannot show equivalence *) |
|
10 ML {* val _ = cheat_equivp := true *} |
8 |
11 |
9 ML {* val _ = recursive := false *} |
12 ML {* val _ = recursive := false *} |
10 nominal_datatype exp6 = |
13 nominal_datatype exp6 = |
11 EVar name |
14 EVar name |
12 | EPair exp6 exp6 |
15 | EPair exp6 exp6 |
26 thm exp6_pat6.eq_iff |
29 thm exp6_pat6.eq_iff |
27 thm exp6_pat6.bn |
30 thm exp6_pat6.bn |
28 thm exp6_pat6.perm |
31 thm exp6_pat6.perm |
29 thm exp6_pat6.induct |
32 thm exp6_pat6.induct |
30 thm exp6_pat6.distinct |
33 thm exp6_pat6.distinct |
|
34 thm exp6_pat6.supp |
31 |
35 |
32 end |
36 end |
33 |
37 |
34 |
38 |
35 |
39 |