NO_THEN
Thm_cont.NO_THEN : thm_tactical
Theorem-tactical which always fails.
When applied to a theorem-tactic and a theorem, the theorem-tactical
NO_THEN always fails with string `NO_THEN`.
Failure
Always fails when applied to a theorem-tactic and a theorem (note that it never gets as far as being applied to a goal!)
Writing compound tactics or tacticals.
See also
Tactical.ALL_TAC,
Thm_cont.ALL_THEN,
Tactical.FAIL_TAC,
Tactical.NO_TAC