equal
deleted
inserted
replaced
341 ]); |
341 ]); |
342 *} |
342 *} |
343 apply (atomize(full)) |
343 apply (atomize(full)) |
344 apply (tactic {* tac @{context} 1 *}) *) |
344 apply (tactic {* tac @{context} 1 *}) *) |
345 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
345 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
346 ML {* |
346 (* ML {* |
347 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
347 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
348 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
348 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
349 *} |
349 *} |
350 (*prove rg |
350 prove rg |
351 apply(atomize(full)) |
351 apply(atomize(full)) |
|
352 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
|
353 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
354 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
355 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
356 |
352 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
357 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
353 done*) |
358 done*) |
354 ML {* val ind_r_t = |
359 ML {* val ind_r_t = |
355 Toplevel.program (fn () => |
360 Toplevel.program (fn () => |
356 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
361 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |