FAIL_LT : string -> list_tactic
STRUCTURE
Tactical
SYNOPSIS
List-tactic which always fails, with the supplied string.
DESCRIPTION
Whatever goal list it is applied to,
FAIL_LT s
always fails with the string
s
.
FAILURE
The application of
FAIL_LT
to a string never fails; the resulting list-tactic always fails.
SEEALSO
FAIL_TAC
,
ALL_LT
,
NO_LT
HOL
Kananaskis-13