----------------------------------------------------------------------
NO_THEN                                                     (Thm_cont)
----------------------------------------------------------------------
NO_THEN : thm_tactical

SYNOPSIS
Theorem-tactical which always fails.

KEYWORDS
theorem-tactic.

DESCRIBE
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!)

USES
Writing compound tactics or tacticals.

SEEALSO
Tactical.ALL_TAC, Thm_cont.ALL_THEN, Tactical.FAIL_TAC,
Tactical.NO_TAC.

----------------------------------------------------------------------