src/HOL/ex/InSort.ML
changeset 3912 4ed64ad7fb42
parent 3647 a64c8fbcd98f
child 3919 c036caebfc75