src/ZF/Induct/Multiset.thy
changeset 41648 6d736d983d5c
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2