SPEC_ALL_TAC : tactic
STRUCTURE
ConseqConv
SYNOPSIS
Generalizes a goal.
DESCRIPTION
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
SPEC_TAC
HOL  Kananaskis-14