TRANSThm.TRANS : (thm -> thm -> thm)Uses transitivity of equality on two equational theorems.
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 = t3Fails unless the theorems are equational, with the right side of the first being the same as the left side of the second.
- 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