Miscellaneous

Cases [t1;...;tn]

Does n-way case split. For example:



 

GenConcl ''

v should be a variable. Generalizes occurrences of t as subterms of the concl to variable v. Adds new hypotheses declaring v to be of type T and stating that .

  ApFunToHypEquands (x:var) (:term) (:term) (i:int)

If hypothesis i is of form , then this tactic applies the function to the terms a and b to give a new hypothesis in the subgoal labelled main of form .  Also creates a couple of aux subgoals. See file inclusion-tactics.ml for details.