THEN_TCL : (thm_tactical * thm_tactical -> thm_tactical)
STRUCTURE
Thm_cont
SYNOPSIS
Composes two theorem-tacticals.
DESCRIPTION
If ttl1 and ttl2 are two theorem-tacticals, ttl1 THEN_TCL ttl2 is a theorem-tactical which composes their effect; that is, if: 
   ttl1 ttac th1 = ttac th2
and 
   ttl2 ttac th2 = ttac th3
then 
   (ttl1 THEN_TCL ttl2) ttac th1 = ttac th3

FAILURE
The application of THEN_TCL to a pair of theorem-tacticals never fails.
SEEALSO
EVERY_TCL, FIRST_TCL, ORELSE_TCL
HOL  Kananaskis-13