Cases : tactic
STRUCTURE
BasicProvers
SYNOPSIS
Case split on leading universally quantified variable in a goal.
DESCRIPTION
bossLib.Cases
is identical to
BasicProof.Cases
.
SEEALSO
Cases
HOL
Kananaskis-14