----------------------------------------------------------------------
CHECK_ASSUME_TAC                                              (Tactic)
----------------------------------------------------------------------
CHECK_ASSUME_TAC : thm_tactic

SYNOPSIS
Adds a theorem to the assumption list of goal, unless it solves the goal.

KEYWORDS
tactic, assumption.

DESCRIBE
When applied to a theorem {A' |- s} and a goal {A ?- t}, the tactic
{CHECK_ASSUME_TAC} checks whether the theorem will solve the goal (this
includes the possibility that the theorem is just {A' |- F}). If so, the goal
is duly solved. If not, the theorem is added to the assumptions of the goal,
unless it is already there.

       A ?- t
   ==============  CHECK_ASSUME_TAC (A' |- F)   [special case 1]


       A ?- t
   ==============  CHECK_ASSUME_TAC (A' |- t)   [special case 2]


       A ?- t
   ==============  CHECK_ASSUME_TAC (A' |- s)   [general case]
    A u {s} ?- t

Unless {A'} is a subset of {A}, the tactic will be invalid, although
it will not fail.

FAILURE
Never fails.

SEEALSO
Tactic.ACCEPT_TAC, Tactic.ASSUME_TAC, Tactic.CONTR_TAC,
Tactic.DISCARD_TAC, Tactic.MATCH_ACCEPT_TAC.

----------------------------------------------------------------------