src/ZF/Induct/Multiset.thy
changeset 69232 2b913054a9cf
parent 63040 eb4ddd18d635
child 69587 53982d5ec0bb