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