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) |