(THEN_TCL) : thm_tactical -> thm_tactical -> thm_tactical

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 CONDITIONS
The application of THEN_TCL to a pair of theorem-tacticals never fails.

SEE ALSO
EVERY_TCL, FIRST_TCL, ORELSE_TCL.