equal
deleted
inserted
replaced
213 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
213 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
214 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
214 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
215 apply(simp add: map_prs) |
215 apply(simp add: map_prs) |
216 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
216 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
217 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *} |
217 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *} |
|
218 apply(simp only: map_prs) |
|
219 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
218 sorry |
220 sorry |
219 |
221 |
220 (* |
222 (* |
221 FIXME: All below is your construction code; mostly commented out as it |
223 FIXME: All below is your construction code; mostly commented out as it |
222 does not work. |
224 does not work. |