src/HOL/Induct/Multiset0.ML
changeset 8434 5e4bba59bfaa
parent 6301 08245f5a436d
child 8935 548901d05a0e