src/Pure/search.ML
changeset 21378 cedfce6fc725
parent 20852 edc3147ab164
child 22025 7c5896919eb8