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