src/Pure/search.ML
changeset 59290 569a8109eeb2
parent 59058 a78612c67ec0
child 59582 0fbed69ff081
equal deleted inserted replaced
59289:42710fe5f05a 59290:569a8109eeb2