----------------------------------------------------------------------
FAIL_TAC                                                    (Tactical)
----------------------------------------------------------------------
FAIL_TAC : string -> tactic

SYNOPSIS
Tactic which always fails, with the supplied string.

KEYWORDS
tactic.

DESCRIBE
Whatever goal it is applied to, {FAIL_TAC s} always fails
with the string {s}.

FAILURE
The application of {FAIL_TAC} to a string never fails; the resulting
tactic always fails.

EXAMPLE
The following example uses the fact that if a tactic {t1} solves
a goal, then the tactic {t1 THEN t2} never results in the application
of {t2} to anything, because {t1} produces no subgoals. In attempting
to solve the following goal:

   ?- if x then T else T

the tactic

   REWRITE_TAC[] THEN FAIL_TAC "Simple rewriting failed to solve goal"

will fail with the message provided, whereas:

   CONV_TAC COND_CONV THEN FAIL_TAC "Using COND_CONV failed to solve goal"

will silently solve the goal because {COND_CONV} reduces it to
just {?- T}.

SEEALSO
Tactical.ALL_TAC, Tactical.NO_TAC.

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