equal
deleted
inserted
replaced
23 thm ty_tys.eq_iff |
23 thm ty_tys.eq_iff |
24 thm ty_tys.fv_bn_eqvt |
24 thm ty_tys.fv_bn_eqvt |
25 thm ty_tys.size_eqvt |
25 thm ty_tys.size_eqvt |
26 thm ty_tys.supports |
26 thm ty_tys.supports |
27 thm ty_tys.supp |
27 thm ty_tys.supp |
|
28 thm ty_tys.fresh |
28 |
29 |
29 (* defined as two separate nominal datatypes *) |
30 (* defined as two separate nominal datatypes *) |
30 |
31 |
31 nominal_datatype ty2 = |
32 nominal_datatype ty2 = |
32 Var2 "name" |
33 Var2 "name" |
44 thm tys2.eq_iff |
45 thm tys2.eq_iff |
45 thm tys2.fv_bn_eqvt |
46 thm tys2.fv_bn_eqvt |
46 thm tys2.size_eqvt |
47 thm tys2.size_eqvt |
47 thm tys2.supports |
48 thm tys2.supports |
48 thm tys2.supp |
49 thm tys2.supp |
49 |
50 thm tys2.fresh |
50 |
51 |
51 |
52 |
52 text {* *} |
53 text {* *} |
53 |
54 |
54 (* |
55 (* |