src/Pure/search.ML
changeset 59389 c427f3de9050
parent 59058 a78612c67ec0
child 59582 0fbed69ff081
equal deleted inserted replaced
59388:04cdfd536e7d 59389:c427f3de9050