src/ZF/Induct/Multiset.thy
changeset 66787 64b47495676d
parent 63040 eb4ddd18d635
child 69587 53982d5ec0bb