----------------------------------------------------------------------
ORELSE_TCL                                                  (Thm_cont)
----------------------------------------------------------------------
ORELSE_TCL : (thm_tactical * thm_tactical -> thm_tactical)

SYNOPSIS
Applies a theorem-tactical, and if it fails, tries a second.

KEYWORDS
theorem-tactical.

DESCRIBE
When applied to two theorem-tacticals, {ttl1} and {ttl2}, a theorem-tactic
{ttac}, and a theorem {th}, if {ttl1 ttac th} succeeds, that gives the
result. If it fails, the result is {ttl2 ttac th}, which may itself fail.

FAILURE
{ORELSE_TCL} fails if both the theorem-tacticals fail when applied to the
given theorem-tactic and theorem.

SEEALSO
Thm_cont.EVERY_TCL, Thm_cont.FIRST_TCL, Thm_cont.THEN_TCL.

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