Documentation

Mathlib.Tactic.Common

This file imports all tactics which do not have significant theory imports, and hence can be imported very low in the theory import hierarchy, thereby making tactics widely available without needing specific imports.

We include some commented out imports here, with an explanation of their theory requirements, to save some time for anyone wondering why they are not here.

Register tactics with hint. #