TRANS : thm -> thm -> thm
A1 |- t1 = t2 A2 |- t2' = t3 -------------------------------- TRANS A1 u A2 |- t1 = t3
# let t1 = ASSUME `a:bool = b` and t2 = ASSUME `b:bool = c`;; val t1 : thm = a <=> b |- a <=> b val t2 : thm = b <=> c |- b <=> c # TRANS t1 t2;; val it : thm = a <=> b, b <=> c |- a <=> c # let t1 = ASSUME `x:num = 1` and t2 = num_CONV `1`;; val t1 : thm = x = 1 |- x = 1 val t2 : thm = |- 1 = SUC 0 # TRANS t1 t2;; val it : thm = x = 1 |- x = SUC 0