(ORELSE) : tactic -> tactic -> tactic

SYNOPSIS
Applies first tactic, and iff it fails, applies the second instead.

DESCRIPTION
If t1 and t2 are tactics, t1 ORELSE t2 is a tactic which applies t1 to a goal, and iff it fails, applies t2 to the goal instead.

FAILURE CONDITIONS
The application of ORELSE to a pair of tactics never fails. The resulting tactic fails if both t1 and t2 fail when applied to the relevant goal.

EXAMPLE
The tactic STRIP_TAC breaks down the logical structure of a goal in various ways, e.g. stripping off universal quantifiers and putting the antecedent of implicational conclusions into the assumptions. However it does not break down equivalences into two implications, as EQ_TAC does. So you might start breaking down a goal corresponding to the inbuilt theorem MOD_EQ_0
  # g `!m n. ~(n = 0) ==> ((m MOD n = 0) <=> (?q. m = q * n))`;;
  ...
as follows
  # e(REPEAT(STRIP_TAC ORELSE EQ_TAC));;
  val it : goalstack = 2 subgoals (2 total)

   0 [`~(n = 0)`]
   1 [`m = q * n`]

  `m MOD n = 0`

   0 [`~(n = 0)`]
   1 [`m MOD n = 0`]

  `?q. m = q * n`

SEE ALSO
EVERY, FIRST, THEN.