RESQ_RES_TAC
res_quanLib.RESQ_RES_TAC : tactic
Enriches assumptions by repeatedly resolving restricted universal quantifications in them against the others.
RESQ_RES_TAC uses those assumptions which are restricted universal
quantifications in resolution in a way similar to RES_TAC. It calls
RESQ_RES_THEN repeatedly until there is no more resolution can be
done. The conclusions of all the new results are returned as additional
assumptions of the subgoal(s). The effect of RESQ_RES_TAC on a goal is
to enrich the assumption set with some of its collective consequences.
Failure
RESQ_RES_TAC cannot fail and so should not be unconditionally
REPEATed.
See also
res_quanLib.RESQ_IMP_RES_TAC,
res_quanLib.RESQ_IMP_RES_THEN,
res_quanLib.RESQ_RES_THEN,
Tactic.IMP_RES_TAC,
Thm_cont.IMP_RES_THEN,
Drule.RES_CANON,
Thm_cont.RES_THEN,
Tactic.RES_TAC