equal
deleted
inserted
replaced
747 *} |
747 *} |
748 |
748 |
749 ML {* |
749 ML {* |
750 fun equals_rsp_tac R ctxt = |
750 fun equals_rsp_tac R ctxt = |
751 let |
751 let |
752 val t = domain_type (fastype_of R); |
752 val ty = domain_type (fastype_of R); |
753 val thy = ProofContext.theory_of ctxt |
753 val thy = ProofContext.theory_of ctxt |
754 val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
754 val thm = Drule.instantiate' |
|
755 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
755 in |
756 in |
756 rtac thm THEN' RANGE [quotient_tac ctxt] |
757 rtac thm THEN' quotient_tac ctxt |
757 end |
758 end |
758 handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac |
759 handle THM _ => K no_tac |
|
760 | TYPE _ => K no_tac |
|
761 | TERM _ => K no_tac |
759 *} |
762 *} |
760 |
763 |
761 ML {* |
764 ML {* |
762 fun rep_abs_rsp_tac ctxt = |
765 fun rep_abs_rsp_tac ctxt = |
763 SUBGOAL (fn (goal, i) => |
766 SUBGOAL (fn (goal, i) => |