----------------------------------------------------------------------
EVERY_TCL                                                   (Thm_cont)
----------------------------------------------------------------------
EVERY_TCL : (thm_tactical list -> thm_tactical)

SYNOPSIS
Composes a list of theorem-tacticals.

KEYWORDS
theorem-tactical.

DESCRIBE
When given a list of theorem-tacticals and a theorem, {EVERY_TCL} simply
composes their effects on the theorem. The effect is:

   EVERY_TCL [ttl1;...;ttln] = ttl1 THEN_TCL ... THEN_TCL ttln

In other words, if:

   ttl1 ttac th1 = ttac th2  ...  ttln ttac thn = ttac thn'

then:

   EVERY_TCL [ttl1;...;ttln] ttac th1 = ttac thn'

If the theorem-tactical list is empty, the resulting theorem-tactical
behaves in the same way as {ALL_THEN}, the identity theorem-tactical.

FAILURE
The application to a list of theorem-tacticals never fails.

SEEALSO
Thm_cont.FIRST_TCL, Thm_cont.ORELSE_TCL, Thm_cont.REPEAT_TCL,
Thm_cont.THEN_TCL.

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