FAIL_TAC : string -> tactic

- STRUCTURE
- 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:the tactic
?- if x then T else T

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"

- SEEALSO

HOL Kananaskis-13