(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 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.