Mathlib Changelog
v4
Changelog
About
Github
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.mkTagAttr
View on Github →
2023-01-19 22:25
Mathlib/Tactic/TagAttr.lean
feat: solve_by_elim using (attributes) (#1581)
Added
Mathlib.Tactic.TagAttr.mkTagAttr
View on Github →