src/ZF/Induct/Multiset.thy
changeset 45048 59ca831deef4
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2