----------------------------------------------------------------------
TRANS                                                            (Thm)
----------------------------------------------------------------------
TRANS : (thm -> thm -> thm)

SYNOPSIS
Uses transitivity of equality on two equational theorems.

KEYWORDS
rule, transitivity, equality.

DESCRIBE
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
Thm.EQ_MP, Drule.IMP_TRANS, Thm.REFL, Thm.SYM.

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