src/HOL/Induct/Multiset.thy
changeset 9356 30c3d3e308ee
parent 9017 ff259b415c4d
child 9659 b9cf6801f3da