TRANS : (thm -> thm -> thm)
STRUCTURE
Thm
SYNOPSIS
Uses transitivity of equality on two equational theorems.
DESCRIPTION
When applied to a theorem A1 |- t1 = t2 and a theorem A2 |- t2 = t3, the inference rule TRANS returns the theorem A1 u A2 |- t1 = t3. 
    A1 |- t1 = t2   A2 |- t2 = t3
   -------------------------------  TRANS
         A1 u A2 |- t1 = t3

FAILURE
Fails unless the theorems are equational, with the right side of the first being the same as the left side of the second.
EXAMPLE
   - val t1 = ASSUME ``a:bool = b`` and t2 = ASSUME ``b:bool = c``;
   val t1 = [.] |- a = b : thm
   val t2 = [.] |- b = c : thm

   - TRANS t1 t2;
   val it = [..] |- a = c : thm

SEEALSO
EQ_MP, IMP_TRANS, REFL, SYM
HOL  Trindemossen-1