src/Pure/search.ML
changeset 21966 edab0ecfbd7c
parent 20852 edc3147ab164
child 22025 7c5896919eb8