VALID : tactic -> tactic
STRUCTURE
SYNOPSIS
Makes a tactic fail if it would otherwise return an invalid proof.
DESCRIPTION
If tac applied to the goal (asl,g) produces a justification that does not create a theorem A |- g, with A a subset of asl, then VALID tac (asl,g) fails (raises an exception). If tac produces a valid proof on the goal, then the behaviour of VALID tac (asl,g) is the same as tac (asl,g)
FAILURE
Fails by design if tac produces an invalid proof when applied to a goal. Also fails if tac fails when applied to the given goal.
SEEALSO
HOL  Trindemossen-1