----------------------------------------------------------------------
GEN_VALIDATE                                                (Tactical)
----------------------------------------------------------------------
GEN_VALIDATE : bool -> tactic -> tactic

SYNOPSIS
Where a tactic requires assumptions to be in the goal,
add those assumptions as new subgoals.

DESCRIBE
See {VALIDATE}, which is implemented as {GEN_VALIDATE true}.

Suppose {tac} applied to the goal {(asl,g)} produces a justification that
creates a theorem {A |- g'}.
Then {GEN_VALIDATE false} adds new subgoals for members of {A},
regardless of whether they are present in {asl}.

FAILURE
Fails by design if {tac}, when applied to a goal,
produces a proof which is invalid on account of proving
a theorem whose conclusion differs from that of the goal.

Also fails if {tac} fails when applied to the given goal.

EXAMPLE
For example, where theorem {uthr'} is {[p', q] |- r}


1 subgoal:
val it =

r
------------------------------------
  0.  p
  1.  q

> e (VALIDATE (ACCEPT_TAC uthr')) ;
OK..
1 subgoal:
val it =

p'
------------------------------------
  p
:
   proof

but, instead of that,

> e (GEN_VALIDATE false (ACCEPT_TAC uthr')) ;
OK..
2 subgoals:
val it =

q
------------------------------------
  0.  p
  1.  q


p'
------------------------------------
  0.  p
  1.  q


USES
Use {GEN_VALIDATE false} rather than {VALIDATE}
when programming compound tactics if you want to know
what the resulting subgoals will be,
 regardless of what the assumptions of the goal are.

SEEALSO
Tactical.VALID, Tactical.VALIDATE, Tactical.ADD_SGS_TAC.

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