FAIL_TAC : string -> tactic
STRUCTURE
Tactical
SYNOPSIS
Tactic which always fails, with the supplied string.
DESCRIPTION
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
ALL_TAC, NO_TAC
HOL  Kananaskis-13