THEN_TCL
Thm_cont.THEN_TCL : (thm_tactical * thm_tactical -> thm_tactical)
Composes two theorem-tacticals.
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.