RESQ_IMP_RES_TAC

res_quanLib.RESQ_IMP_RES_TAC : thm_tactic

Repeatedly resolves a restricted universally quantified theorem with the assumptions of a goal.

The function RESQ_IMP_RES_TAC performs repeatedly resolution using a restricted quantified theorem. It takes a restricted quantified theorem and transforms it into an implication. This resulting theorem is used in the resolution.

Given a theorem th, the theorem-tactic RESQ_IMP_RES_TAC applies RESQ_IMP_RES_THEN repeatedly to resolve the theorem with the assumptions.

Failure

Never fails

See also

res_quanLib.RESQ_IMP_RES_THEN, res_quanLib.RESQ_RES_THEN, res_quanLib.RESQ_RES_TAC, Thm_cont.IMP_RES_THEN, Tactic.IMP_RES_TAC, Drule.MATCH_MP, Drule.RES_CANON, Tactic.RES_TAC, Thm_cont.RES_THEN