----------------------------------------------------------------------
SPEC_ALL_TAC                                              (ConseqConv)
----------------------------------------------------------------------
SPEC_ALL_TAC : tactic

SYNOPSIS
Generalizes a goal.

KEYWORDS
tactic.

DESCRIBE
When applied to a goal {A ?- t}, the tactic {SPEC_ALL_TAC} generalizes
all variables that are free in {t}, but not in {A}. This results in a
goal of the form {A ?- !x1 ... xn. t}.

           A ?- t
   ====================  SPEC_ALL_TAC
    A ?- !x1 ... xn. t


EXAMPLE

   - val _ = set_goal ([``(P x):bool``], ``Q x /\ Z y``)
   > Initial goal:

     Q x /\ Z y
     ------------------------------------
       P x

   - e(SPEC_ALL_TAC)
   >
     !Q Z y. Q x /\ Z y
     ------------------------------------
       P x


FAILURE
{SPEC_ALL_TAC} never fails. However, maybe no variable is generalized.

SEEALSO
Tactic.SPEC_TAC.

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