----------------------------------------------------------------------
ALL_THEN                                                    (Thm_cont)
----------------------------------------------------------------------
ALL_THEN : thm_tactical

SYNOPSIS
Passes a theorem unchanged to a theorem-tactic.

KEYWORDS
theorem-tactic, identity.

DESCRIBE
For any theorem-tactic {ttac} and theorem {th}, the application
{ALL_THEN ttac th} results simply in {ttac th}, that is, the theorem
is passed unchanged to the theorem-tactic. {ALL_THEN} is the identity
theorem-tactical.

FAILURE
The application of {ALL_THEN} to a theorem-tactic never fails. The resulting
theorem-tactic fails under exactly the same conditions as the original one.

USES
Writing compound tactics or tacticals, e.g. terminating list iterations
of theorem-tacticals.

SEEALSO
Tactical.ALL_TAC, Tactical.FAIL_TAC, Tactical.NO_TAC,
Thm_cont.NO_THEN, Thm_cont.THEN_TCL, Thm_cont.ORELSE_TCL.

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