(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.