src/HOL/ex/Sorting.ML
changeset 4655 481628ea8edd
parent 4089 96fba19bcbe2
child 4686 74a12e86b20b