THEN_TCL : (thm_tactical * thm_tactical -> thm_tactical)
STRUCTURE
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
HOL  Kananaskis-13