src/Pure/search.ML
changeset 80303 11fee9e6ba43
parent 62919 9eb0359d6a77
child 81954 6f2bcdfa9a19
equal deleted inserted replaced
80302:d1c7da4ff0f5 80303:11fee9e6ba43