src/ZF/Induct/Multiset.thy
changeset 61763 96d2c1b9a30a
parent 61393 8673ec68c798
child 61798 27f3c10b0b50