--- a/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 nominal_datatype tkind =
   KStar
@@ -88,72 +88,15 @@
 (* can lift *)
 
 thm distinct
+thm induct
+thm exhaust
 thm fv_defs
-thm alpha_bn_imps alpha_equivp
-
-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 bn_defs
 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)
-
 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 _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
-*}
-
-ML {* 
-  val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{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.induct})
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
-*}
+thm fv_bn_eqvt
+thm size_eqvt
 
-ML {* 
-  val thms_i = map (lift_thm @{context} qtys []) @{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 @{context} qtys []) @{thms perm_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}
-*}
-
-ML {*
-  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
-    prod.cases}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
-*}