(ORELSE_TCL) : thm_tactical -> thm_tactical -> thm_tactical

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

DESCRIPTION
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 CONDITIONS
ORELSE_TCL fails if both the theorem-tacticals fail when applied to the given theorem-tactic and theorem.

SEE ALSO
EVERY_TCL, FIRST_TCL, THEN_TCL.