Declare this tactic to be an alias or alternative form of an existing tactic.
This has the following effects:
- The alias relationship is saved
- The docstring is taken from the original tactic, if present
Equations
Instances For
Add one or more tags to a tactic.
Tags should be applied to the canonical names for tactics.