src/Pure/search.ML
changeset 21924 fe474e69e603
parent 20852 edc3147ab164
child 22025 7c5896919eb8