SUFF_TAC : term -> tactic
STRUCTURE
SYNOPSIS
Introduces an implicational subgoal.
DESCRIPTION
A call to SUFF_TAC t on the goal asl ?- g introduces two subgoals: asl ?- t ==> g and asl ?- t. At a high-level, the user’s claim is that term t suffices (hence the name) to prove the goal. The first new goal to be discharged is the check for this; the second is to actually show t.
FAILURE
Will fail if t is not of type :bool.
SEEALSO
HOL  Kananaskis-13