src/HOL/Induct/Multiset0.thy
changeset 10257 21055ac27708
parent 5628 15b7f12ad919