- 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