mathlib3
e1eba9fa - chore(tactic/*): clean up doc tags (#15563)

Commit

3 years ago

chore(tactic/*): clean up doc tags (#15563) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author

robertylewis

Parents