mathlib3
feat(tactic/interactive): move `rotate` into interactive namespace
#1272

Merged

feat(tactic/interactive): move `rotate` into interactive namespace #1272

mergify merged 1 commit into leanprover-community:master from jesse-michael-han:rotate

feat(tactic/interactive): move `rotate` into interactive namespace

22e6960d

jesse-michael-han requested a review 6 years ago

jcommelin approved these changes on 2019-07-28

jcommelin added ready-to-merge

mergify merged 9689f4d5 into master 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone