equal
deleted
inserted
replaced
717 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
717 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
718 in |
718 in |
719 (rtac inst_thm THEN' quotient_tac ctxt) i |
719 (rtac inst_thm THEN' quotient_tac ctxt) i |
720 end |
720 end |
721 handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *) |
721 handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *) |
|
722 (* The catch was for an error of solve_quotient_assum. You replaced it by quotient_tac |
|
723 so I suppose it is equivalent to a "SOLVES" around quotient_tac. *) |
722 | _ => no_tac) |
724 | _ => no_tac) |
723 *} |
725 *} |
724 |
726 |
725 ML {* |
727 ML {* |
726 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
728 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |