src/HOL/ex/InSort.ML
changeset 4571 6b02fc8a97f6
parent 4089 96fba19bcbe2
child 4686 74a12e86b20b