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