src/ZF/Induct/Multiset.thy
changeset 36416 9459be72b89e
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2