src/HOL/Induct/Multiset.thy
changeset 9750 270cd9831e7b
parent 9659 b9cf6801f3da