equal
deleted
inserted
replaced
80 | "bv_tvtk TVTKNil = {}" |
80 | "bv_tvtk TVTKNil = {}" |
81 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
81 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
82 | "bv_tvck TVCKNil = {}" |
82 | "bv_tvck TVCKNil = {}" |
83 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*) |
83 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*) |
84 |
84 |
|
85 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_tvtk_lst_tvck_lst_vt_lst.fv |
|
86 |
|
87 |
85 end |
88 end |
86 |
89 |
87 |
90 |
88 |
91 |