`LABEL_TAC : string -> thm_tactic`

SYNOPSIS
Add an assumption with a named label to a goal.

DESCRIPTION
Given a theorem th, the tactic LABEL_TAC "name" th will add th as a new hypothesis, just as ASSUME_TAC does, but will also give it name as a label. The name will show up when the goal is printed, and can be used to refer to the theorem in tactics like USE_THEN and REMOVE_THEN.

FAILURE CONDITIONS
Never fails, though may be invalid if the theorem has assumptions that are not a subset of those in the goal, up to alpha-equivalence.

EXAMPLE
Suppose we want to prove that a binary relation <<= that is antisymmetric and has a strong wellfoundedness property is also total and transitive, and hence a wellorder:
```  # g `(!x y. x <<= y /\ y <<= x ==> x = y) /\
(!s. ~(s = {}) ==> ?a:A. a IN s /\ !x. x IN s ==> a <<= x)
==> (!x y. x <<= y \/ y <<= x) /\
(!x y z. x <<= y /\ y <<= z ==> x <<= z)`;;
```
We might start by putting the two hypotheses on the assumption list with intuitive names:
```  # e(DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "antisym") (LABEL_TAC "wo")));;
val it : goalstack = 1 subgoal (1 total)

0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)

`(!x y. x <<= y \/ y <<= x) /\ (!x y z. x <<= y /\ y <<= z ==> x <<= z)`
```
Now we break down the goal a bit
```  # e(REPEAT STRIP_TAC);;
val it : goalstack = 2 subgoals (2 total)

0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)
2 [`x <<= y`]
3 [`y <<= z`]

`x <<= z`

0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)

`x <<= y \/ y <<= x`
```
We want to specialize the wellordering assumption to an appropriate set for each case, and we can identify it using the label wo; the problem is then simple set-theoretic reasoning:
```  # e(USE_THEN "wo" (MP_TAC o SPEC `{x:A,y:A}`) THEN SET_TAC[]);;
...
val it : goalstack = 1 subgoal (1 total)

0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)
2 [`x <<= y`]
3 [`y <<= z`]

`x <<= z`
```
Similarly for the other one:
```  # e(USE_THEN "wo" (MP_TAC o SPEC `{x:A,y:A,z:A}`) THEN ASM SET_TAC[]);;
...
val it : goalstack = No subgoals
```

USES
Convenient for referring to an assumption explicitly, just as in mathematics books one sometimes marks a theorem with an asterisk or dagger, then refers to it using that symbol.