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.