src/HOL/Induct/MultisetOrder.thy
changeset 9789 7e5e6c47c0b5
parent 9660 80d14ea0e200