src/Pure/search.ML
changeset 21277 ac2d7e03a3b1
parent 20852 edc3147ab164
child 22025 7c5896919eb8