src/HOL/ex/Qsort.ML
changeset 12436 a2df07fefed7
parent 9747 043098ba5098
equal deleted inserted replaced
12435:a42be4b09cc3 12436:a2df07fefed7