src/HOL/ex/InSort.ML
changeset 1228 7d6b0241afab
parent 969 b051e2fc2e34
child 1266 3ae9fe3c0f68