IMP_RES_FORALL_CONV : conv
STRUCTURE
res_quanTools
SYNOPSIS
Converts an implication to a restricted universal quantification.
DESCRIPTION
When applied to a term of the form !x.P x ==> Q, the conversion IMP_RES_FORALL_CONV returns the theorem: 
   |- (!x. P x ==> Q) = !x::P. Q
FAILURE
Fails if applied to a term not of the form !x.P x ==> Q.
SEEALSO
RES_FORALL_CONV
HOL  Kananaskis-10