Nominal/ExCoreHaskell.thy
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