# Add solver `multiset_solver` for multisets

The code contains some documentation how it works.

I added a number of tests, and used it to automate many existing lemmas in the `gmultiset`

file.

Note that this required restructuring the file quite a bit, since I needed some basic lemmas (now in section `basic_lemmas`

) to define the tactic, and wanted to use the tactic subsequently to prove many of the existing lemmas (now in section `multiset_unfold`

). None of the lemma statements changed, only many proofs are replaced by a mere call to `multiset_solver`

.

/cc @msammler

Edited by Robbert Krebbers