KNOW_TAC
Tactic.KNOW_TAC : term -> tactic
A shorthand form of SUBGOAL_THEN.
A call to KNOW_TAC t is equivalent to a call to
SUBGOAL_THEN t MP_TAC.
Failure
A call to KNOW_TAC t will fail on being applied to a goal if the
provided term t is not of boolean type.
Comments
If t is to be created through parsing a user-provided string, it may
be helpful to do that parsing in the context of the current goal, for
which Q_TAC may be helpful.
Equally, the by and suffices_by tactics have a similar effect:
taking a quotation, and generating two subgoals to be proved. In all
cases, the behaviour is to give the user an opportunity to be creative
in the specification of the fresh sub-goal that arises from applying
modus ponens backwards.
See also
bossLib.by, Tactical.Q_TAC,
Tactic.SUBGOAL_THEN,
Tactic.SUFF_TAC,
bossLib.suffices_by