----------------------------------------------------------------------
THEN_TCL                                                    (Thm_cont)
----------------------------------------------------------------------
THEN_TCL : (thm_tactical * thm_tactical -> thm_tactical)

SYNOPSIS
Composes two theorem-tacticals.

KEYWORDS
theorem-tactical.

DESCRIBE
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
Thm_cont.EVERY_TCL, Thm_cont.FIRST_TCL, Thm_cont.ORELSE_TCL.

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