ORELSE_TCL : (thm_tactical * thm_tactical -> thm_tactical)
STRUCTURE
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
ORELSE_TCL fails if both the theorem-tacticals fail when applied to the given theorem-tactic and theorem.
SEEALSO
HOL  Kananaskis-13