src/HOL/Induct/Multiset0.thy
changeset 7142 89e0ff71d113
parent 5628 15b7f12ad919