Interactive versions of tactics

Stream: general

[Seul Baek]

Is it considered good practice to put interactive versions of tactics in tactic/interactive.lean instead of in their respective files?

I didn't do this for omega, but this seems to be the way most other interactive tactics are organized.

[Mario Carneiro]

See ring for example. You should open a little interactive namespace (Simon added a user command recently to make this easier, although it may not yet have landed) at the end of your main file and define the command there. Don't put it in tactic.interactive unless it's a lightweight tactic

[Simon Hudon]

I think what you're referring to is in #878, which still needs some work