src/HOL/ex/ImperativeQuicksort.thy
changeset 28172 a46751a649af
parent 28145 af3923ed4786
child 29399 ebcd69a00872