Commit 2020-06-10 15:54 f7654b3f
View on Github →feat(tactic/generalizes): tactic for generalizing over multiple expressions (#2982)
This commit adds a tactic generalizes which works like generalize but for multiple expressions at once. The tactic is more powerful than calling generalize multiple times since this usually fails when there are dependencies between the expressions. By contrast, generalizes handles at least some such situations.