----------------------------------------------------------------------
SPEC_UNDISCH_EXL                                               (Drule)
----------------------------------------------------------------------
SPEC_UNDISCH_EXL : thm -> thm

SYNOPSIS
Strips universal quantifiers and antecedents of implications
(splitting conjunctive antecedents),
then where possible replaces the formerly quantified variables
as existentials in the new hypotheses.

KEYWORDS
universal, existential, quantifier, assumption, hypothesis

DESCRIBE
In this example, assume that {a1} and {a3} (only) involve the free variable {x}.

   |- !x. a1 ==> !y. a2 ==> !z. a3 ==> !u. t
   ----------------------------------------- SPEC_UNDISCH_EXL
	   ?x. a1 /\ a3, a2 |- t


FAILURE
No failure.  Can leave the supplied theorem unchanged.

COMMENTS
See {EXISTS_LEFT} for more on the existential quantification aspect.
Note that the existential quantification happens only for variables
which were universally quantified in the supplied theorem
(to get around this limitation, first apply {GEN_ALL} to the supplied theorem).

EXAMPLE
Where {trans_thm} is {[] |- !x y z. (x = y) ==> (y = z) ==> (x = z)}

{SPEC_UNDISCH_EXL trans_thm} is {[?y. (x = y) /\ (y = z)] |- x = z}

SEEALSO
Drule.EXISTS_LEFT, Tactic.irule.

----------------------------------------------------------------------