src/HOL/Induct/Multiset0.thy
changeset 9369 139fde7af7bd
parent 5628 15b7f12ad919