src/ZF/Induct/Multiset.thy
changeset 24825 c4f13ab78f9d
parent 20898 113c9516a2d7
child 24892 c663e675e177