NO_TAC : tactic
STRUCTURE
SYNOPSIS
Tactic which always fails.
DESCRIPTION
Whatever goal it is applied to, NO_TAC always fails with string `NO_TAC`.
FAILURE
Always fails.
SEEALSO
HOL  Kananaskis-14