Def Mathlib.Tactic.TagAttr.mkTagAttr

Modification history

2023-02-13 18:09
Mathlib/Tactic/TagAttr.lean
chore: rename register_tag_attr, and explain relation to registerTagAttribute (#2124) …
Deleted Mathlib.Tactic.TagAttr.mkTagAttrView on Github →
2023-01-19 22:25
Mathlib/Tactic/TagAttr.lean
feat: solve_by_elim using (attributes) (#1581)
Added Mathlib.Tactic.TagAttr.mkTagAttrView on Github →