equal
deleted
inserted
replaced
658 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
658 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
659 *} |
659 *} |
660 |
660 |
661 ML {* |
661 ML {* |
662 (* FIXME / TODO: what is asmf and asma in the code below *) |
662 (* FIXME / TODO: what is asmf and asma in the code below *) |
663 |
663 (* asmf is the QUOT_TRUE assumption function |
|
664 asma are QUOT_TRUE assumption arguments *) |
664 val apply_rsp_tac = |
665 val apply_rsp_tac = |
665 Subgoal.FOCUS (fn {concl, asms, context,...} => |
666 Subgoal.FOCUS (fn {concl, asms, context,...} => |
666 let |
667 let |
667 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
668 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
668 val qt_asm = find_qt_asm (map term_of asms) |
669 val qt_asm = find_qt_asm (map term_of asms) |
717 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
718 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
718 in |
719 in |
719 (rtac inst_thm THEN' quotient_tac ctxt) i |
720 (rtac inst_thm THEN' quotient_tac ctxt) i |
720 end |
721 end |
721 handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *) |
722 handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *) |
|
723 (* The catch was for an error of solve_quotient_assum. You replaced it by quotient_tac |
|
724 so I suppose it is equivalent to a "SOLVES" around quotient_tac. *) |
722 | _ => no_tac) |
725 | _ => no_tac) |
723 *} |
726 *} |
724 |
727 |
725 ML {* |
728 ML {* |
726 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
729 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |