17.2. Minimizing grind calls

The grind only [...] tactic invokes grind with a limited set of theorems, which can improve performance. Calls to grind only can be conveniently constructed using grind?, which automatically records the theorems used by grind and suggests a suitable grind only.

These theorems will typically include a symbol prefix such as =, ←, or →, indicating the pattern that triggered the instantiation. See the section on E-matching for details. Some theorems may be labelled with a usr prefix, which indicates that a custom pattern was used.