src/ZF/Induct/Multiset.thy
changeset 68147 a8f40dd73c61
parent 63040 eb4ddd18d635
child 69587 53982d5ec0bb