--- a/Nominal/Ex/CoreHaskell.thy	Sun Aug 15 11:03:13 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sun Aug 15 14:00:28 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 18]]
+declare [[STEPS = 20]]
 
 nominal_datatype tkind =
   KStar
@@ -85,10 +85,50 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-
+(* can lift *)
 thm distinct
+thm fv_defs
 
-term TvsNil
+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.inducts
+thm perm_simps
+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
+
+ML {*
+  val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co},
+              @{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars},
+              @{typ tvars}, @{typ cvars}]
+*}
+
+ML {*
+  val thms_d = map (lift_thm qtys @{context}) @{thms distinct}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm qtys @{context}) @{thms 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.inducts}
+*}
+
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm qtys @{context}) @{thms 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)}
+*}
+
+ML {*
+  val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps}
+*}
+
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}
+*}
+
+
 
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)