src/HOL/ex/InSort.thy
changeset 5078 7b5ea59c0275
parent 1896 df4e40b9ff6d
child 5184 9b8547a9496a