--- a/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 18:17:53 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Aug 18 00:19:15 2010 +0800
@@ -86,6 +86,7 @@
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
 (* can lift *)
+
 thm distinct
 thm fv_defs
 thm alpha_bn_imps alpha_equivp
@@ -95,7 +96,6 @@
 thm perm_laws
 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)
 
-(* cannot lift yet *)
 thm eq_iff
 thm eq_iff_simps