RES_FORALL_CONV : conv
STRUCTURE
res_quanLib
SYNOPSIS
Converts a restricted universal quantification to an implication.
DESCRIPTION
When applied to a term of the form
!x::P. Q
, the conversion
RES_FORALL_CONV
returns the theorem:
|- !x::P. Q = (!x. x IN P ==> Q)
which is the underlying semantic representation of the restricted universal quantification.
FAILURE
Fails if applied to a term not of the form
!x::P. Q
.
SEEALSO
IMP_RES_FORALL_CONV
HOL
Trindemossen-1