Kethku opened this issue 9 years ago · 0 comments
Same issue as with find_rewrite. Should be made more consistent. This was also the place where people said Tactic Notations would be good. I don't know what that means though.