src/ZF/Induct/Multiset.thy
changeset 15388 aa785cea8fff
parent 15201 d73f9d49d835
child 15481 fc075ae929e4