namedCases : string list -> tactic
STRUCTURE
BasicProvers
SYNOPSIS
Case split on type of leading universally quantified variable in the goal, using given names for introduced constructor arguments.
DESCRIPTION
bossLib.namedCases
is identical to
BasicProvers.namedCases
.
SEEALSO
namedCases_on
,
Cases_on
,
Cases
HOL
Kananaskis-14