HOL-Theorem-Prover/HOL — pull request #217 by jeremydaw (2014-12-20 10:08:57+00:00)
Title: GEN_VALIDATE(_LT) - flag for adding new subgoals in any event

GEN_VALIDATE false is like VALIDATE, but adds subgoals for the assumptions
of the theorem produced by the justification, regardless of whether they
are among the assumptions of the goal. Advantage of this is that
GEN_VALIDATE false (ACCEPT_TAC th) produces predictable subgoals,
which may help in coding compound tactics