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:
will fail with the message provided, whereas:
REWRITE_TAC THEN FAIL_TAC "Simple rewriting failed to solve goal"
will silently solve the goal because COND_CONV reduces it to
just ?- T.
CONV_TAC COND_CONV THEN FAIL_TAC "Using COND_CONV failed to solve goal"