ORELSE_TCLThm_cont.ORELSE_TCL : (thm_tactical * thm_tactical -> thm_tactical)Applies a theorem-tactical, and if it fails, tries a second.
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.
ORELSE_TCL fails if both the theorem-tacticals fail when
applied to the given theorem-tactic and theorem.