namedCases_on : term quotation -> string list -> tactic
STRUCTURE
BasicProvers
SYNOPSIS
Case split on type of supplied term, using given names for introduced constructor arguments.
DESCRIPTION
bossLib.namedCases_on
is identical to
BasicProvers.namedCases_on
.
SEEALSO
namedCases
,
Cases_on
,
Cases
HOL
Kananaskis-14