RESQ_HALF_SPEC : (thm -> thm)
STRUCTURE
res_quanTools
SYNOPSIS
Strip a restricted universal quantification in the conclusion of a theorem.
DESCRIPTION
When applied to a theorem A |- !x::P. t, the derived inference rule RESQ_HALF_SPEC returns the theorem A |- !x. P x ==> t, i.e., it transforms the restricted universal quantification to its underlying semantic representation. 
      A |- !x::P. t
   --------------------  RESQ_HALF_SPEC
    A |- !x. P x ==> t
FAILURE
Fails if the theorem’s conclusion is not a restricted universal quantification.
SEEALSO
RESQ_SPEC, RESQ_SPECL
HOL  Kananaskis-10