src/Pure/search.ML
changeset 59140 e7f28b330cb2
parent 59058 a78612c67ec0
child 59582 0fbed69ff081