src/ZF/Induct/Multiset.thy
changeset 17740 fc385ce6187d
parent 16973 b2a894562b8f
child 18415 eb68dc98bda2