KNOW_TAC : term -> tactic
STRUCTURE
Tactic
SYNOPSIS
A shorthand form of SUBGOAL_THEN.
DESCRIPTION
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.

SEEALSO
by, Q_TAC, SUBGOAL_THEN, SUFF_TAC, suffices_by
HOL  Trindemossen-1