1\DOC
2
3\TYPE {VALID : tactic -> tactic}
4
5\SYNOPSIS
6Makes a tactic fail if it would otherwise return an invalid proof.
7
8\DESCRIBE
9If {tac} applied to the goal {(asl,g)} produces a justification that
10does not create a theorem {A |- g}, with {A} a subset of {asl}, then
11{VALID tac (asl,g)} fails (raises an exception).  If {tac} produces a
12valid proof on the goal, then the behaviour of {VALID tac (asl,g)} is
13the same as {tac (asl,g)}
14
15\FAILURE
16Fails by design if {tac} produces an invalid proof when applied
17to a goal.  Also fails if {tac} fails when applied to the given goal.
18
19\SEEALSO
20proofManagerLib.expand, Tactical.VALIDATE.
21
22\ENDDOC
23