342 

   342 

   343 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}

   343 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}

   344 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}

   344 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}

   345 

   345 

   346 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}

   346 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}

   347 

   348 

   348 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *}

   349 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *}

   349 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}

   350 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}

   350 

   351 

   351 

   352 

   384 ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *}

   385 ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *}

   385 ML {*

   386 ML {*

   386   val rt = build_repabs_term @{context} t_r consts rty qty

   387   val rt = build_repabs_term @{context} t_r consts rty qty

   387   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);

   388   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);

   388 *}

   389 *}

   394 apply(atomize(full))

   391 apply(atomize(full))

   395 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}

   392 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}

   396 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

   393 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

   397 

   394 

   398 done

   395 done