Tactics and Automation
There are two parts to this chapter. The first part presents several collections of tactics specialized in various domains of logic and mathematics: tactics specialized in reasoning about inductive types, the main automatic tactics, which rely on a Prolog-like proof search mechanism, the tactics for equality and rewriting, the tactics for numerical proofs, and the automatic decision procedures for restricted fragments of logic.
Unable to display preview. Download preview PDF.