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 Kananaskis-13