src/Pure/search.ML
changeset 21012 f08574148b7a
parent 20852 edc3147ab164
child 22025 7c5896919eb8