subgoal : term quotation -> tactic
STRUCTURE
bossLib
SYNOPSIS
Produces a subgoal.
DESCRIPTION
A call to
subgoal q
is equivalent (by definition) to a call to
Q.SUBGOAL_THEN q STRIP_ASSUME_TAC
.
FAILURE
Fails if the provided quotation does not parse to a term of boolean type in the context of the current goal.
COMMENTS
The
subgoal
tactic is also available via the name
sg
.
SEEALSO
by
,
SUBGOAL_THEN
HOL
Kananaskis-14