equal
deleted
inserted
replaced
221 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t},t_r] *} |
221 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t},t_r] *} |
222 ML {* val abs = findabs rty (prop_of t_a) *} |
222 ML {* val abs = findabs rty (prop_of t_a) *} |
223 ML {* val aps = findaps rty (prop_of t_a); *} |
223 ML {* val aps = findaps rty (prop_of t_a); *} |
224 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
224 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
225 |
225 |
226 (*ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *}*) |
226 (*ML {* val t_t = repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms *}*) |
227 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *} |
227 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *} |
228 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
228 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
229 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
229 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
230 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
230 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
231 ML {* val defs_sym = add_lower_defs @{context} defs *} |
231 ML {* val defs_sym = add_lower_defs @{context} defs *} |