src/ZF/Induct/Multiset.thy
changeset 45107 76fef3e57004
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2