src/HOL/Induct/Multiset0.thy
changeset 7333 6cb15c6f1d9f
parent 5628 15b7f12ad919