PURE_CASE_TAC : tactic
STRUCTURE
SYNOPSIS
Case splits on a term t that features in the goal as case t of ....
DESCRIPTION
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
HOL  Kananaskis-13