src/ZF/Induct/Multiset.thy
changeset 35186 bb64d089c643
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2