src/HOL/ex/InSort.thy
changeset 4153 e534c4c32d54
parent 1896 df4e40b9ff6d
child 5184 9b8547a9496a