`TRANS_TAC : thm -> term -> tactic`

SYNOPSIS
Applies transitivity theorem to goal with chosen intermediate term.

DESCRIPTION
When applied to a `transitivity' theorem, i.e. one of the form
```   |- !xs. R1 x y /\ R2 y z ==> R3 x z
```
and a term t, TRANS_TAC produces a tactic that reduces a goal with conclusion of the form R3 s u to one with conclusion R1 s t /\ R2 t u.
```       A ?- R3 s u
========================  TRANS_TAC (|- !xs. R1 x y /\ R2 y z ==> R3 x z) `t`
A ?- R1 s t /\ R2 t u
```

EXAMPLE
Consider the simple inequality goal:
```  # g `n < (m + 2) * (n + 1)`;;
```
We can use the following transitivity theorem
```  # LET_TRANS;;
val it : thm = |- !m n p. m <= n /\ n < p ==> m < p
```
```  # e(TRANS_TAC LET_TRANS `1 * (n + 1)`);;
val it : goalstack = 1 subgoal (1 total)

`n <= 1 * (n + 1) /\ 1 * (n + 1) < (m + 2) * (n + 1)`
```

FAILURE CONDITIONS
Fails unless the input theorem is of the expected form (some of the relations R1, R2 and R3 may be, and often are, the same) and the conclusion matches the goal, in the usual sense of higher-order matching.