11 declare [[STEPS = 20]]

    11 declare [[STEPS = 21]]

    92 thm alpha_bn_imps alpha_equivp

    94 thm bn_defs

    93 

    94 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

   100 thm eq_iff_simps

    97 thm fv_bn_eqvt

   101 

    98 thm size_eqvt

   102 ML {*

    99 

   103   val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co},

   104               @{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars},

   105               @{typ tvars}, @{typ cvars}]

   106 *}

   107 

   108 

   109 ML {*

   110   val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})

   111 *}

   112 

   113 ML {* 

   114   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})

   115 *}

   116 

   117 ML {*

   118   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}

   119 *}

   120 

   121 ML {* 

   122   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)}

   123 *}

   124 

   125 ML {*

   126   val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}

   127 *}

   128 

   129 ML {*

   130   val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}

   131 *}

   132 

   133 ML {*

   134   val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

   135     prod.cases}

   136 *}

   137 

   138 ML {*

   139  val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff}

   140 *}

   141 

   142 ML {*

   143   val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}

   144 *}

   145 

   146 ML {*

   147   val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}

   148 *}

   149 

   150 ML {*

   151   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}

   152 *}

   153 

   154 ML {*

   155   val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}

   156 *}