VALID : tactic -> tactic
STRUCTURE
Tactical
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
FAILURE
Fails by design if its argument produces an invalid proof when applied to a goal. Also fails if its argument fails when applied to the given proof.
SEEALSO
expand
HOL  Kananaskis-10