NO_TAC
Tactical.NO_TAC : tactic
Tactic which always fails.
Whatever goal it is applied to, NO_TAC always fails with string
`NO_TAC`.
Failure
Always fails.
See also
Tactical.ALL_TAC,
Thm_cont.ALL_THEN,
Tactical.FAIL_TAC,
Thm_cont.NO_THEN