src/HOL/ex/Sorting.ML
changeset 3564 f886dbd91ee5
parent 3465 e85c24717cad
child 3647 a64c8fbcd98f