FAIL_TAC : string -> tactic
Tactic which always fails, with the supplied string.
Whatever goal it is applied to, FAIL_TAC s always fails with the string s.
The application of FAIL_TAC to a string never fails; the resulting tactic always fails.
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.
HOL  Kananaskis-13