Cases_on : term quotation -> tactic
STRUCTURE
SYNOPSIS
Performs case analysis on the type of a given term.
LIBRARY
BasicProvers
DESCRIPTION
An application Cases_on M performs a case-split based on the type ty of M, using the cases theorem for ty from the global TypeBase database.

Cases_on can be used to specify variables that are buried in the quantifier prefix. Cases_on can also be used to perform case splits on non-variable terms. If M is a non-variable term that does not occur bound in the goal, then the cases theorem is instantiated with M and used to generate as many sub-goals as there are disjuncts in the cases theorem.

FAILURE
Fails if ty does not have a case theorem in the TypeBase.
EXAMPLE
None yet.
SEEALSO
HOL  Trindemossen-1