src/HOL/Induct/Multiset.ML
changeset 9356 30c3d3e308ee
parent 9266 1b917b8b1b38
child 9747 043098ba5098