`ASSUME_TAC : thm_tactic`

SYNOPSIS
Adds an assumption to a goal.

DESCRIPTION
Given a theorem th of the form A' |- u, and a goal, ASSUME_TAC th adds u to the assumptions of the goal.
```         A ?- t
==============  ASSUME_TAC (A' |- u)
A u {u} ?- t
```
Note that unless A' is a subset of A, this tactic is invalid. The new assumption is unlabelled; for a named assumption use LABEL_TAC.

FAILURE CONDITIONS
Never fails.

EXAMPLE
One can add an external theorem as an assumption if desired, for example so that ASM_REWRITE_TAC[] will automatically apply it. But usually the theorem is derived from some theorem-tactical, e.g. by discharging the antecedent of an implication or doing forward inference on another assumption. For example iff faced with the goal:
```  # g `0 = x ==> f(2 * x) = f(x * f(x))`;;
```
one might not want to just do DISCH_TAC or STRIP_TAC because the assumption will be `0 = x`. One can swap it first then put it on the assumptions by:
```  # e(DISCH_THEN(ASSUME_TAC o SYM));;
val it : goalstack = 1 subgoal (1 total)

0 [`x = 0`]

`f (2 * x) = f (x * f x)`
```
after which the goal can very easily be solved:
```  # e(ASM_REWRITE_TAC[MULT_CLAUSES]);;
val it : goalstack = No subgoals
```

USES
Useful as a parameter to various theorem-tacticals such as X_CHOOSE_THEN, DISCH_THEN etc. when it is simply desired to add the theorem that has been deduced to the assumptions rather than used further at once.