GEN_VALIDATE : bool -> tactic -> tactic
STRUCTURE
Tactical
SYNOPSIS
Where a tactic requires assumptions to be in the goal, add those assumptions as new subgoals.
DESCRIPTION
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
VALID, VALIDATE, ADD_SGS_TAC
HOL  Kananaskis-14