RESQ_RES_THEN : thm_tactic -> tactic
STRUCTURE
res_quanTools
SYNOPSIS
Resolves all restricted universally quantified assumptions against other assumptions of a goal.
DESCRIPTION
Like the function RESQ_IMP_RES_THEN, the function RESQ_RES_THEN performs a single step resolution. The difference is that the restricted universal quantification used in the resolution is taken from the assumptions.

Given a theorem-tactic ttac, applying the tactic RESQ_RES_THEN ttac to a goal (asml,gl) has the effect of: 

   MAP_EVERY (mapfilter ttac [... ; (ai,aj |- vi) ; ...]) (amsl ?- g)
where the theorems ai,aj |- vi are all the consequences that can be drawn by a (single) matching modus-ponens inference from the assumptions amsl and the implications derived from the restricted universal quantifications in the assumptions.
FAILURE
Evaluating RESQ_RES_TAC ttac th fails if there are no restricted universal quantifications in the assumptions, or if the theorem-tactic ttac applied to all the consequences fails.

SEEALSO
RESQ_IMP_RES_TAC, RESQ_IMP_RES_THEN, RESQ_RES_TAC, IMP_RES_THEN, IMP_RES_TAC, MATCH_MP, RES_CANON, RES_TAC, RES_THEN
HOL  Kananaskis-10