equal
deleted
inserted
replaced
65 thm baz.perm_simps |
65 thm baz.perm_simps |
66 thm baz.eq_iff |
66 thm baz.eq_iff |
67 thm baz.fv_bn_eqvt |
67 thm baz.fv_bn_eqvt |
68 thm baz.size_eqvt |
68 thm baz.size_eqvt |
69 thm baz.supp |
69 thm baz.supp |
|
70 |
|
71 (* |
|
72 a nominal datatype with a set argument of |
|
73 pure type |
|
74 *) |
70 |
75 |
|
76 nominal_datatype set_ty = |
|
77 Set_ty "nat set" |
|
78 | Fun "nat \<Rightarrow> nat" |
|
79 | Var "name" |
|
80 | Lam x::"name" t::"set_ty" bind x in t |
|
81 |
|
82 thm set_ty.distinct |
|
83 thm set_ty.induct |
|
84 thm set_ty.exhaust |
|
85 thm set_ty.strong_exhaust |
|
86 thm set_ty.fv_defs |
|
87 thm set_ty.bn_defs |
|
88 thm set_ty.perm_simps |
|
89 thm set_ty.eq_iff |
|
90 thm set_ty.fv_bn_eqvt |
|
91 thm set_ty.size_eqvt |
|
92 thm set_ty.supp |
71 |
93 |
72 end |
94 end |
73 |
95 |
74 |
96 |
75 |
97 |