changeset 1615 | 0ea578c6dae3 |
parent 1609 | c9bc3b61046c |
child 1621 | a40dbea68d0b |
--- a/Nominal/ExCoreHaskell.thy Tue Mar 23 11:43:09 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Tue Mar 23 16:28:29 2010 +0100 @@ -82,6 +82,9 @@ | "bv_tvck TVCKNil = {}" | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*) +thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_tvtk_lst_tvck_lst_vt_lst.fv + + end