----------------------------------------------------------------------
PURE_CASE_TAC                                           (BasicProvers)
----------------------------------------------------------------------
PURE_CASE_TAC : tactic

SYNOPSIS
Case splits on a term {t} that features in the goal as {case t of ...}.

DESCRIBE
{BasicProvers.PURE_CASE_TAC} searches the goal for an instance of
{case t of ...}, and performs a {BasicProvers.Cases_on `t`}.

FAILURE
{BasicProvers.PURE_CASE_TAC} fails if there is no instance of
{case t of ...} in the goal, where the {case} term is a case constant in
the typebase and all the free variables of {t} are free in the goal.

SEEALSO
BasicProvers.CASE_TAC.

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