src/ZF/Induct/Multiset.thy
changeset 76406 40a365360680
parent 76217 8655344f1cf6
child 80754 701912f5645a