----------------------------------------------------------------------
CASE_TAC                                                (BasicProvers)
----------------------------------------------------------------------
CASE_TAC : tactic

SYNOPSIS
Case splits on a term {t} that features in the goal as {case t of ...},
and then performs some simplification.

DESCRIBE
{BasicProvers.CASE_TAC} first calls {BasicProvers.PURE_CASE_TAC}, which
searches the goal for an instance of {case t of ...} and performs a
{BasicProvers.Cases_on `t`}. If this succeeds, it then simplifies the
goal using definitions of {case} constants, plus distinctness and
injectivity theorems for datatypes.

COMMENTS
When there are multiple {case} constants in the goal, it can be very
convenient to execute the tactic {REPEAT CASE_TAC}. {bossLib.CASE_TAC}
is the same as {BasicProvers.CASE_TAC}.

FAILURE
{BasicProvers.CASE_TAC} fails precisely when {BasicProvers.PURE_CASE_TAC}
fails.

SEEALSO
BasicProvers.PURE_CASE_TAC.

----------------------------------------------------------------------