Commit 2019-09-23 17:36 87d1240f
View on Github →feat(tactic/core): derive handler for simple instances (#1475)
- feat(tactic/core): derive handler for simple algebraic instances
- change comment
- use mk_definition
- Update src/tactic/core.lean Co-Authored-By: Johan Commelin johan@commelin.net