SUBGOAL_TAC : string -> term -> tactic list -> tactic

SYNOPSIS
Encloses the sub-proof of a named lemma.

DESCRIPTION
The call SUBGOAL_TAC "name" `t` [tac] introduces a new subgoal t with the current assumptions, runs on that subgoal the tactic tac, and attaches the result as a new hypothesis called name in the current subgoal. The [tac] argument is always a one-element list, for stylistic reasons. If tac does not prove the goal, any resulting subgoals from it will appear first.

FAILURE CONDITIONS
Fails if t is not Boolean or if tac fails on it.

EXAMPLE
If we want to prove
  # g `(n MOD 2) IN {0,1}`;;
we might start by establishing a lemma:
  # e(SUBGOAL_TAC "ml2" `n MOD 2 < 2` [SIMP_TAC[DIVISION; ARITH]]);;
  val it : goalstack = 1 subgoal (1 total)

   0 [`n MOD 2 < 2`] (ml2)

  `n MOD 2 IN {0, 1}`
after which, for example, we could finish things with
  # e(REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
      POP_ASSUM MP_TAC THEN ARITH_TAC);;
  val it : goalstack = No subgoals

USES
Structuring proofs via a sequence of simple lemmas.

SEE ALSO
SUBGOAL_THEN.